Superquadratic sensitivity separation: tournament cyclic

Constructs the cyclic tournament on Fin (2 * a + 1), with an edge i → j exactly when the cyclic difference (j - i).val lies between 1 and a. Every vertex has outdegree a, so taking a = M ^ 2 gives a regular tournament on 2 * M ^ 2 + 1 vertices, as required by the recursive construction.

Main definitions

• cyclicTournament: the cyclic tournament on Fin (2 * a + 1).
• regularCyclicTournament: the cyclic tournament on 2 * M ^ 2 + 1 vertices, viewed as a regular tournament.

Main results

• cyclicTournament_outdegree: every vertex of cyclicTournament a has outdegree a.

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.cyclicTournament (a : ℕ) : Tournament (2 * a + 1)

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.cyclicTournament_outdegree (a : ℕ) (i : Fin (2 * a + 1)) : (Finset.filter ((cyclicTournament a).Adj i) Finset.univ).card = a

Every vertex of cyclicTournament a has exactly a outgoing neighbors.

def Cslib.QueryComplexity.SensitivitySeparation.Internal.regularCyclicTournament (M : ℕ) : RegularTournament M

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