Superquadratic sensitivity separation: recursive zero

Bounds the sensitivity of the recursive family at inputs where it is false. A sensitive bit must repair the unique failed condition of some row clause: of a target candidate (at most 15), of the gate sink (at most one), or of a non-sink gate candidate (at most 3). In the last case the gate witness is itself a gate candidate, so the flip changes both the gate and the final predicate on a single child, which is charged to the joint sensitivity.

Main results

• recursive_sensitivity_zero_at: at an input with output false, the sensitivity is at most 15 * sideSensitivity F false + sideSensitivity F true + 3 * jointSensitivity F true.
• recursive_side_zero: the same bound for the false-side sensitivity of the recursive family.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_sensitivity_zero_at {k r h : ℕ} {I : Type} [Fintype I] (T : Tournament k) (A : GoodLabeling T r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (hr : 0 < r) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (hx : recursiveFamily T A.label F q x = false) : sensitivityAt (recursiveFamily T A.label F q) x ≤ 15 * sideSensitivity F false + sideSensitivity F true + 3 * jointSensitivity F true

For a good labeling A, a nested family F and 0 < r, at an input x where recursiveFamily T A.label F q is false, its sensitivity at x is at most 15 * sideSensitivity F false + sideSensitivity F true + 3 * jointSensitivity F true.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_side_zero {k r h : ℕ} {I : Type} [Fintype I] (T : Tournament k) (A : GoodLabeling T r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (hr : 0 < r) : sideSensitivity (recursiveFamily T A.label F) false ≤ 15 * sideSensitivity F false + sideSensitivity F true + 3 * jointSensitivity F true

Zero-side recurrence: for a good labeling, a nested family F and 0 < r, sideSensitivity (recursiveFamily T A.label F) false is at most 15 * sideSensitivity F false + sideSensitivity F true + 3 * jointSensitivity F true.