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. Real-valued forms record the chain k ^ 16 / r ^ 104 ≤ 3 ^ 16 / M ^ 20 < 1, in particular for r = Nat.ceil (Real.sqrt M).

Main results

• labeling_power_bound: (2 * M ^ 2 + 1) ^ 16 < r ^ 104 whenever 3 ≤ M ≤ r ^ 2.
• labeling_union_bound_real: (2 * M ^ 2 + 1) ^ 16 / r ^ 104 ≤ 3 ^ 16 / M ^ 20 < 1 in ℝ.
• labeling_source_estimate: the same chain of estimates with r = Nat.ceil (Real.sqrt M), passing through (3 * M ^ 2) ^ 16 / (Real.sqrt M) ^ 104.

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.

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

If 3 ≤ M and M ≤ r ^ 2, then in ℝ one has (2 * M ^ 2 + 1) ^ 16 / r ^ 104 ≤ 3 ^ 16 / M ^ 20 and 3 ^ 16 / M ^ 20 < 1.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.labeling_source_estimate {M : ℕ} (hM : 3 ≤ M) : ↑((2 * M ^ 2 + 1) ^ 16) / ↑⌈√↑M⌉₊ ^ 104 ≤ (3 * ↑M ^ 2) ^ 16 / √↑M ^ 104 ∧ (3 * ↑M ^ 2) ^ 16 / √↑M ^ 104 = 3 ^ 16 / ↑M ^ 20 ∧ 3 ^ 16 / ↑M ^ 20 < 1

For 3 ≤ M, with r = Nat.ceil (Real.sqrt M): (2 * M ^ 2 + 1) ^ 16 / r ^ 104 ≤ (3 * M ^ 2) ^ 16 / (Real.sqrt M) ^ 104, the latter equals 3 ^ 16 / M ^ 20, and 3 ^ 16 / M ^ 20 < 1.