Superquadratic sensitivity separation: labeling bounds

Two elementary numerical facts used in the union bound for good labelings: every natural number M is at most the square of Nat.ceil (Real.sqrt M), so this many labels satisfy M ≤ r ^ 2, and for M ≥ 3 a tournament on 2 * M ^ 2 + 1 vertices has at least 120 = Nat.choose 16 2 ordered pairs of vertices.

Main results

• le_ceil_sqrt_sq: M ≤ (Nat.ceil (Real.sqrt M)) ^ 2.
• labeling_space_large: 120 ≤ (2 * M ^ 2 + 1) * (2 * M ^ 2 + 1) for 3 ≤ M.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.le_ceil_sqrt_sq (M : ℕ) : M ≤ ⌈√↑M⌉₊ ^ 2

Every natural number satisfies M ≤ (Nat.ceil (Real.sqrt M)) ^ 2.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.labeling_space_large {M : ℕ} (hM : 3 ≤ M) : 120 ≤ (2 * M ^ 2 + 1) * (2 * M ^ 2 + 1)

For 3 ≤ M, 120 ≤ (2 * M ^ 2 + 1) * (2 * M ^ 2 + 1).