Superquadratic sensitivity separation: seed amplification

Combines the depth-nine seed with M = 9 ^ 10 and power amplification. The seed has sensitivity at most 22 * M ^ 10 and block sensitivity at least M ^ 2 * (2 * M ^ 2 + 1) ^ 9 at the all-false input, a strict quadratic gap, so its iterated compositions form a family with a fixed exponent α > 2 such that s ^ α ≤ bs, with ratio bs / s ^ 2 ≥ (128 / 121) ^ m and unbounded block sensitivity.

Main results

• constructed_power_family: a family of nonconstant functions with s ^ α ≤ bs for a fixed α > 2, ratio bs / s ^ 2 ≥ (128 / 121) ^ m, and block sensitivity tending to infinity.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.constructed_power_family : ∃ (α : ℝ), 2 < α ∧ ∃ (n : ℕ → ℕ) (F : (m : ℕ) → (Fin (n m) → Bool) → Bool), (∀ (m : ℕ), 0 < n m ∧ (F m fun (x : Fin (n m)) => false) = false ∧ (∃ (x : Fin (n m) → Bool) (y : Fin (n m) → Bool), F m x ≠ F m y) ∧ ↑(sensitivity (F m)) ^ α ≤ ↑(blockSensitivityAt (F m) fun (x : Fin (n m)) => false) ∧ (128 / 121) ^ m ≤ ↑(blockSensitivity (F m)) / ↑(sensitivity (F m)) ^ 2) ∧ Filter.Tendsto (fun (m : ℕ) => ↑(blockSensitivityAt (F m) fun (x : Fin (n m)) => false)) Filter.atTop Filter.atTop

There are α > 2 and Boolean functions F m on n m > 0 variables, each nonconstant and vanishing at the all-false input, such that sensitivity (F m) ^ α ≤ blockSensitivityAt (F m) (fun _ => false) and (128 / 121) ^ m ≤ blockSensitivity (F m) / sensitivity (F m) ^ 2 for every m, and blockSensitivityAt (F m) (fun _ => false) tends to infinity.