Superquadratic sensitivity separation: recursive sets

This file packages the sensitive coordinates of individual children as finite sets of raw coordinates, so that the sensitivity of a next-level predicate can be bounded by the size of a union of such sets. It also proves the joint version of the flip analysis: a flip that changes the clause of row i at two indices changes its target condition, or changes both gate conditions on the same labeled edge.

Main definitions

• childLift: the embedding of a set A of coordinates into the component j of J × I.
• childChanges: the raw coordinates of the child (j, c) whose flip changes F q on that child.
• childJointChanges: the raw coordinates of the child (j, c) whose flip changes both F q and F q' on that child.

Main results

• childChanges_card: childChanges F q x j c has as many elements as the sensitivity of F q at the child (j, c).
• childJointChanges_card: childJointChanges F q q' x j c has as many elements as the joint sensitivity of F q and F q' at the child (j, c).
• card_biUnion_le_mul: a union of A.card sets of size at most n has at most A.card * n elements.
• rowClause_joint_flip_change: a flip changing a row clause at two indices changes its target condition or both gate conditions on one labeled edge.

References

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

def Cslib.QueryComplexity.SensitivitySeparation.Internal.childLift {J I : Type} (j : J) (A : Finset I) : Finset (J × I)

Embed a coordinate block into a specified child of a product.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.mem_childLift {J I : Type} (j : J) (A : Finset I) (p : J × I) : p ∈ childLift j A ↔ p.1 = j ∧ p.2 ∈ A

A pair p lies in childLift j A iff p.1 = j and p.2 ∈ A.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.childLift_card {J I : Type} (j : J) (A : Finset I) : (childLift j A).card = A.card

childLift j A has the same cardinality as A.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.childChanges {k r h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) : Finset ((Fin k × Fin r) × I)

Lift the individually sensitive coordinates of a child predicate.

noncomputable def Cslib.QueryComplexity.SensitivitySeparation.Internal.childJointChanges {k r h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (q q' : Fin h) (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) : Finset ((Fin k × Fin r) × I)

Lift coordinates that simultaneously change two predicates in one child.

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.childChanges_card {k r h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) : (childChanges F q x j c).card = sensitivityAt (F q) (recursiveChild x j c)

The cardinality of childChanges F q x j c is sensitivityAt (F q) (recursiveChild x j c).

@[simp]

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.childJointChanges_card {k r h : ℕ} {I : Type} [Fintype I] (F : Fin h → (I → Bool) → Bool) (q q' : Fin h) (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) : (childJointChanges F q q' x j c).card = jointSensitivityAt (F q) (F q') (recursiveChild x j c)

The cardinality of childJointChanges F q q' x j c is jointSensitivityAt (F q) (F q') (recursiveChild x j c).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.card_biUnion_le_mul {J I : Type} [DecidableEq I] (A : Finset J) (B : J → Finset I) (n : ℕ) (hn : ∀ j ∈ A, (B j).card ≤ n) : (A.biUnion B).card ≤ A.card * n

If (B j).card ≤ n for every j ∈ A, then (A.biUnion B).card ≤ A.card * n.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowClause_joint_flip_change {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q q' : Fin h) (x : (Fin k × Fin r) × I → Bool) (i j : Fin k) (c : Fin r) (a : I) (hc : rowClause T label F q (flip x {((j, c), a)}) i ≠ rowClause T label F q x i) (hc' : rowClause T label F q' (flip x {((j, c), a)}) i ≠ rowClause T label F q' x i) : j = i ∧ F (Fin.last h) (flip (recursiveChild x j c) {a}) ≠ F (Fin.last h) (recursiveChild x j c) ∨ T.Adj i j ∧ c = label i j ∧ F (gateIndex q) (flip (recursiveChild x j c) {a}) ≠ F (gateIndex q) (recursiveChild x j c) ∧ F (gateIndex q') (flip (recursiveChild x j c) {a}) ≠ F (gateIndex q') (recursiveChild x j c)

If flipping ((j, c), a) changes the clause of row i both at index q and at index q', then either j = i and the flip changes the target value of the child at (j, c), or T.Adj i j, c = label i j and the flip changes both gate values F (gateIndex q) and F (gateIndex q') of that child.