Sensitivity separation: tournament

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Tournament.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

structure Complexity.BooleanAnalysis.Sensitivity.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 Complexity.BooleanAnalysis.Sensitivity.Internal.RegularTournament (M : ℕ) extends Complexity.BooleanAnalysis.Sensitivity.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 Complexity.BooleanAnalysis.Sensitivity.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 Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.ne_of_adj {k : ℕ} (T : Tournament k) {i j : Fin k} (h : T.Adj i j) : i ≠ j

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.not_adj_reverse {k : ℕ} (T : Tournament k) {i j : Fin k} (h : T.Adj i j) : ¬T.Adj j i

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.Tournament.adj_or_reverse {k : ℕ} (T : Tournament k) {i j : Fin k} (h : i ≠ j) : T.Adj i j ∨ T.Adj j i

theorem Complexity.BooleanAnalysis.Sensitivity.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

theorem Complexity.BooleanAnalysis.Sensitivity.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