Superquadratic sensitivity separation: quantitative profiles

Quantitative bounds for arbitrary natural-number side profiles S and joint profiles J satisfying the four raw recurrences of the recursive construction. Normalizing with normalizedMax and solving the coupled scalar recurrences shows that the zero-side profile grows at most like M ^ n and the one-side profile like M ^ (n + 1), losing only a factor 2 relative to the initial bound L.

Main results

• quantitative_profile_bounds: under the budget max r 16 / M * 3 ^ (d + 1) ≤ 2, profiles satisfying the four recurrences obey S n false ≤ 2 * L * M ^ n and S n true ≤ 2 * L * M ^ (n + 1) for n ≤ d.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.quantitative_profile_bounds (d L M r : ℕ) (hM : 0 < M) (hbudget : ↑(max r 16) / ↑M * 3 ^ (d + 1) ≤ 2) (S J : ℕ → Bool → ℕ) (hS₀ : S 0 false ≤ L) (hS₁ : S 0 true ≤ L * M) (hJ₀ : J 0 false = 0) (hJ₁ : J 0 true = 0) (hstepS₀ : ∀ n < d, S (n + 1) false ≤ 16 * S n false + S n true + 3 * J n true) (hstepS₁ : ∀ n < d, S (n + 1) true ≤ M ^ 2 * S n false + r * S n true) (hstepJ₀ : ∀ n < d, J (n + 1) false ≤ 16 * S n false + 3 * J n true) (hstepJ₁ : ∀ n < d, J (n + 1) true ≤ M ^ 2 * J n false + r * S n true) (n : ℕ) : n ≤ d → S n false ≤ 2 * L * M ^ n ∧ S n true ≤ 2 * L * M ^ (n + 1)

Suppose 0 < M, max r 16 / M * 3 ^ (d + 1) ≤ 2, S 0 false ≤ L, S 0 true ≤ L * M, J 0 false = J 0 true = 0, and for all n < d the profiles satisfy the four raw recurrences. Then S n false ≤ 2 * L * M ^ n and S n true ≤ 2 * L * M ^ (n + 1) for all n ≤ d.