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

• Tournament.goodLabeling_exists_of_power_bound: a good labeling with r labels exists when 0 < r, 120 ≤ k * k and k ^ 16 < r ^ 104.
• goodLabeling_exists: every tournament on 2 * M ^ 2 + 1 vertices has a good labeling with r labels when 3 ≤ M ≤ r ^ 2.
• regular_goodLabeling_exists: the regular cyclic tournament has a good labeling with Nat.ceil (Real.sqrt M) labels for 3 ≤ M.
• GoodLabeling.good_on_subset: the goodness property for target maps defined only on the sixteen-element subset.

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.Tournament.goodLabeling_exists_of_power_bound {k r : ℕ} (T : Tournament k) (hr : 0 < r) (hN : 120 ≤ k * k) (hkr : k ^ 16 < r ^ 104) : Nonempty (GoodLabeling T r)

If 0 < r, 120 ≤ k * k and k ^ 16 < r ^ 104, then T admits a good labeling with r labels.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.goodLabeling_exists {M r : ℕ} (hM : 3 ≤ M) (hMr : M ≤ r ^ 2) (T : Tournament (2 * M ^ 2 + 1)) : Nonempty (GoodLabeling T r)

If 3 ≤ M and M ≤ r ^ 2, then every tournament on 2 * M ^ 2 + 1 vertices admits a good labeling with r labels.

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.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.GoodLabeling.good_on_subset {k r : ℕ} {T : Tournament k} (A : GoodLabeling T r) (I : Finset (Fin k)) (hI : I.card = 16) (m : ↥I → Fin r) : ∃ i ∈ I, ∃ (j : Fin k) (hj : j ∈ I), T.Adj i j ∧ A.label i j ≠ m ⟨j, hj⟩

Goodness for targets defined on the subset: for every I with I.card = 16 and every m : I → Fin r there is an edge i → j of T with i, j ∈ I and A.label i j ≠ m ⟨j, hj⟩.