Superquadratic sensitivity separation: labeling estimate

Numerical estimates showing that the union bound over sixteen-vertex labeling events succeeds. For 3 ≤ M and M ≤ r ^ 2, a tournament on k = 2 * M ^ 2 + 1 vertices satisfies k ^ 16 < r ^ 104, which is exactly what is needed to beat the number of bad labelings.

Main results

• labeling_power_bound: (2 * M ^ 2 + 1) ^ 16 < r ^ 104 whenever 3 ≤ M ≤ r ^ 2.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.labeling_power_bound {M r : ℕ} (hM : 3 ≤ M) (hMr : M ≤ r ^ 2) : (2 * M ^ 2 + 1) ^ 16 < r ^ 104

If 3 ≤ M and M ≤ r ^ 2, then (2 * M ^ 2 + 1) ^ 16 < r ^ 104.