Superquadratic sensitivity separation: recursive one

This file proves the recurrences for the profiles of the next-level family at output true. At an accepted input some row clause holds, and only flips inside its r target children or its o labeled gate children (one per out-neighbour) can make the next-level predicate reject. Counting the sensitive coordinates of these children bounds the side profile by o * sideSensitivity F false + r * sideSensitivity F true, and the joint profile by the same expression with jointSensitivity F false in place of sideSensitivity F false.

Main results

• recursive_sensitivity_one_at: pointwise sensitivity bound at an accepted input.
• recursive_side_one: the side profile of the next-level family at true is at most o * sideSensitivity F false + r * sideSensitivity F true.
• recursive_joint_one_at: pointwise joint sensitivity bound at an input accepted at two indices.
• recursive_joint_one: for nested F, the joint profile of the next-level family at true is at most o * jointSensitivity F false + r * sideSensitivity F true.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_sensitivity_one_at {k r h : ℕ} {I : Type} [Fintype I] (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (o : ℕ) (ho : ∀ (i : Fin k), (Finset.filter (T.Adj i) Finset.univ).card = o) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (hx : recursiveFamily T label F q x = true) : sensitivityAt (recursiveFamily T label F q) x ≤ o * sideSensitivity F false + r * sideSensitivity F true

If every vertex of T has outdegree o and the next-level predicate at index q accepts x, then its sensitivity at x is at most o * sideSensitivity F false + r * sideSensitivity F true.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_side_one {k r h : ℕ} {I : Type} [Fintype I] (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (o : ℕ) (ho : ∀ (i : Fin k), (Finset.filter (T.Adj i) Finset.univ).card = o) : sideSensitivity (recursiveFamily T label F) true ≤ o * sideSensitivity F false + r * sideSensitivity F true

If every vertex of T has outdegree o, then the side profile of the next-level family at true is at most o * sideSensitivity F false + r * sideSensitivity F true.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_joint_one_at {k r h : ℕ} {I : Type} [Fintype I] (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (o : ℕ) (ho : ∀ (i : Fin k), (Finset.filter (T.Adj i) Finset.univ).card = o) (q q' : Fin h) (hqq : q < q') (x : (Fin k × Fin r) × I → Bool) (hx : recursiveFamily T label F q x = true) (hx' : recursiveFamily T label F q' x = true) : jointSensitivityAt (recursiveFamily T label F q) (recursiveFamily T label F q') x ≤ o * jointSensitivity F false + r * sideSensitivity F true

Let F be nested and every vertex of T have outdegree o. If q < q' and the next-level predicates at q and q' both accept x, then their joint sensitivity at x is at most o * jointSensitivity F false + r * sideSensitivity F true.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursive_joint_one {k r h : ℕ} {I : Type} [Fintype I] (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (o : ℕ) (ho : ∀ (i : Fin k), (Finset.filter (T.Adj i) Finset.univ).card = o) : jointSensitivity (recursiveFamily T label F) true ≤ o * jointSensitivity F false + r * sideSensitivity F true

If F is nested and every vertex of T has outdegree o, then the joint profile of the next-level family at true is at most o * jointSensitivity F false + r * sideSensitivity F true.