Superquadratic sensitivity separation: labeling

A counting argument proves that good edge labelings exist. If 0 < r, 120 ≤ k * k and k ^ 16 < r ^ 104, the bad labelings for sixteen vertices are fewer than all r ^ (k * k) labelings, and any labeling avoiding them is good. Specializing to k = 2 * M ^ 2 + 1 gives a good labeling of the regular cyclic tournament with Nat.ceil (Real.sqrt M) labels for every M ≥ 3.

Main results

• regular_goodLabeling_exists: the regular cyclic tournament has a good labeling with Nat.ceil (Real.sqrt M) labels for 3 ≤ M.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.regular_goodLabeling_exists {M : ℕ} (hM : 3 ≤ M) : Nonempty (GoodLabeling (regularCyclicTournament M).toTournament ⌈√↑M⌉₊)

For 3 ≤ M, the regular cyclic tournament on 2 * M ^ 2 + 1 vertices admits a good labeling with Nat.ceil (Real.sqrt M) labels.