Superquadratic sensitivity separation: tournament

Defines tournaments on Fin k, regular tournaments on 2 * M ^ 2 + 1 vertices with outdegree M ^ 2, and good labelings: edge labelings label : Fin k → Fin k → Fin r such that no sixteen vertices admit a target assignment m with label i j = m j on every internal edge i → j. Basic facts about edge orientations and sinks are recorded.

Main definitions

• Tournament: a loopless digraph on Fin k with exactly one edge between distinct vertices.
• RegularTournament: a tournament on 2 * M ^ 2 + 1 vertices of outdegree M ^ 2.
• GoodLabeling: an edge labeling admitting no target-constant set of sixteen vertices.

Main results

• Tournament.adj_or_reverse: distinct vertices are joined in one of the two directions.
• Tournament.internal_sink_unique: a vertex set has at most one internal sink.
• GoodLabeling.good_implies_card_lt_sixteen: a set on which the labeling is target-constant has fewer than 16 vertices.

References

• Adapted from OpenAI's formalization [OAI26b] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Combinatorics/Sensitivity/Tournament.lean), via the complexitylib port [Sch26e] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

structure Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament (k : ℕ) extends Digraph (Fin k) : Type

A loopless directed graph with exactly one edge between distinct vertices.

• Adj : Fin k → Fin k → Prop
• loopless (i : Fin k) : ¬self.Adj i i

  No vertex has an edge to itself.

• edge_compl {i j : Fin k} : i ≠ j → (self.Adj i j ↔ ¬self.Adj j i)

  Exactly one orientation occurs between distinct vertices.

structure Cslib.QueryComplexity.SensitivitySeparation.Internal.RegularTournament (M : ℕ) extends Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament (2 * M ^ 2 + 1) : Type

A tournament on 2 * M ^ 2 + 1 vertices with uniform outdegree M ^ 2.

• Adj : Fin (2 * M ^ 2 + 1) → Fin (2 * M ^ 2 + 1) → Prop
• loopless (i : Fin (2 * M ^ 2 + 1)) : ¬self.Adj i i
• edge_compl {i j : Fin (2 * M ^ 2 + 1)} : i ≠ j → (self.Adj i j ↔ ¬self.Adj j i)
• outdegree (i : Fin (2 * M ^ 2 + 1)) : (Finset.filter (self.Adj i) Finset.univ).card = M ^ 2

  Every vertex has the prescribed number of outgoing neighbors.

structure Cslib.QueryComplexity.SensitivitySeparation.Internal.GoodLabeling {k : ℕ} (T : Tournament k) (r : ℕ) : Type

An edge labeling obstructing every target-constant labeling on sixteen vertices.

• label : Fin k → Fin k → Fin r

  Label assigned to each ordered pair of vertices.

• good (I : Finset (Fin k)) : I.card = 16 → ∀ (m : Fin k → Fin r), ∃ i ∈ I, ∃ j ∈ I, T.Adj i j ∧ self.label i j ≠ m j

  Every sixteen-vertex target assignment disagrees on a directed edge.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.ne_of_adj {k : ℕ} (T : Tournament k) {i j : Fin k} (h : T.Adj i j) : i ≠ j

Adjacent vertices are distinct.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.not_adj_reverse {k : ℕ} (T : Tournament k) {i j : Fin k} (h : T.Adj i j) : ¬T.Adj j i

An edge i → j excludes the reverse edge j → i.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.adj_or_reverse {k : ℕ} (T : Tournament k) {i j : Fin k} (h : i ≠ j) : T.Adj i j ∨ T.Adj j i

Distinct vertices are joined by an edge in at least one of the two directions.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.Tournament.internal_sink_unique {k : ℕ} (T : Tournament k) {I : Finset (Fin k)} {i j : Fin k} (hi : i ∈ I) (hj : j ∈ I) (hsi : ∀ v ∈ I, ¬T.Adj i v) (hsj : ∀ v ∈ I, ¬T.Adj j v) : i = j

Two vertices of a set I, neither having an outgoing edge into I, are equal.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.GoodLabeling.good_implies_card_lt_sixteen {k r : ℕ} {T : Tournament k} (A : GoodLabeling T r) (I : Finset (Fin k)) (m : Fin k → Fin r) (h : ∀ i ∈ I, ∀ j ∈ I, T.Adj i j → A.label i j = m j) : I.card < 16

If A.label i j = m j for every edge i → j inside I, for some target assignment m, then I has fewer than 16 vertices.