Sensitivity separation: tournament cyclic

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

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

def Complexity.BooleanAnalysis.Sensitivity.Internal.cyclicTournament (a : ℕ) : Tournament (2 * a + 1)

Orient the odd cyclic graph by the first half of the nonzero cyclic differences.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.cyclicTournament a = { Adj := fun (i j : Fin (2 * a + 1)) => 0 < ↑(j - i) ∧ ↑(j - i) ≤ a, loopless := ⋯, edge_compl := ⋯ }

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.cyclicTournament_outdegree (a : ℕ) (i : Fin (2 * a + 1)) : (Finset.filter ((cyclicTournament a).Adj i) Finset.univ).card = a

def Complexity.BooleanAnalysis.Sensitivity.Internal.regularCyclicTournament (M : ℕ) : RegularTournament M

The cyclic tournament on 2 * M^2 + 1 vertices has outdegree M^2.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.regularCyclicTournament M = { toTournament := Complexity.BooleanAnalysis.Sensitivity.Internal.cyclicTournament (M ^ 2), outdegree := ⋯ }