Superquadratic sensitivity separation: constructed seed

Instantiates the construction with concrete parameters: the regular cyclic tournament on 2 * M ^ 2 + 1 vertices, Nat.ceil (Real.sqrt M) labels, and a good labeling coming from the union bound. For 1 ≤ d and 9 ^ (d + 1) ≤ M this yields, without further hypotheses, a nonconstant Boolean function vanishing at the all-false input with sensitivity at most 2 * (d + 2) * M ^ (d + 1) and block sensitivity at the all-false input at least M ^ 2 * (2 * M ^ 2 + 1) ^ d.

Main results

• construction_label_count_pos: 0 < Nat.ceil (Real.sqrt M) for 0 < M.
• exists_constructed_seed: a nonconstant seed function with sensitivity at most 2 * (d + 2) * M ^ (d + 1) and block sensitivity at least M ^ 2 * (2 * M ^ 2 + 1) ^ d at the all-false input.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.construction_label_count_pos {M : ℕ} (hM : 0 < M) : 0 < ⌈√↑M⌉₊

For 0 < M, the number of labels Nat.ceil (Real.sqrt M) is positive.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.exists_constructed_seed (d M : ℕ) (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : ∃ (f : (Fin (constructionDimension d M ⌈√↑M⌉₊) → Bool) → Bool), 0 < constructionDimension d M ⌈√↑M⌉₊ ∧ (f fun (x : Fin (constructionDimension d M ⌈√↑M⌉₊)) => false) = false ∧ (∃ (x : Fin (constructionDimension d M ⌈√↑M⌉₊) → Bool) (y : Fin (constructionDimension d M ⌈√↑M⌉₊) → Bool), f x ≠ f y) ∧ sensitivity f ≤ 2 * (d + 2) * M ^ (d + 1) ∧ M ^ 2 * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt f fun (x : Fin (constructionDimension d M ⌈√↑M⌉₊)) => false

For 1 ≤ d and 9 ^ (d + 1) ≤ M there is a nonconstant Boolean function f on constructionDimension d M (Nat.ceil (Real.sqrt M)) > 0 variables with f (fun _ => false) = false, sensitivity f ≤ 2 * (d + 2) * M ^ (d + 1) and M ^ 2 * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt f (fun _ => false).