Superquadratic sensitivity separation: recursive joint zero

Bounds the joint sensitivity of two indices q < q' of the recursive family at an input where both are false. A bit changing both outputs makes some row clause true at the stronger index q', hence also at the weaker index q, so it repairs a failed condition with respect to the candidate lists of q: either of a target candidate (at most 15) or of a gate candidate (at most 3), in which case the flip changes both gate predicates F (gateIndex q') and F (gateIndex q) on a single child.

Main results

• recursive_joint_zero_at: at an input where both indices give false, the joint sensitivity is at most 15 * sideSensitivity F false + 3 * jointSensitivity F true.
• recursive_joint_zero: the same bound for the false-side joint sensitivity of the recursive family.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_joint_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 q' : Fin h) (hqq : q < q') (x : (Fin k × Fin r) × I → Bool) (hx : recursiveFamily T A.label F q x = false) (hx' : recursiveFamily T A.label F q' x = false) : jointSensitivityAt (recursiveFamily T A.label F q) (recursiveFamily T A.label F q') x ≤ 15 * sideSensitivity F false + 3 * jointSensitivity F true

For a good labeling A, a nested family F, 0 < r and indices q < q' at which recursiveFamily T A.label F is false on x, the joint sensitivity of the two predicates at x is at most 15 * sideSensitivity F false + 3 * jointSensitivity F true.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_joint_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) : jointSensitivity (recursiveFamily T A.label F) false ≤ 15 * sideSensitivity F false + 3 * jointSensitivity F true

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