Superquadratic sensitivity separation: recursive flips

This file analyses the effect of a single raw bit flip on a row clause. Flipping the coordinate ((j, c), a) changes only the child at (j, c). Hence it can change the clause of row i only if j = i and it changes the target value of that child, or if j is an out-neighbour of i, c = label i j and it changes the gate value of that child. These facts underlie all sensitivity recurrences.

Main results

• recursiveChild_flip_same: flipping ((j, c), a) flips coordinate a of the child at (j, c).
• recursiveChild_flip_other: flipping ((j, c), a) leaves every other child unchanged.
• rowClause_flip_eq: a flip that changes none of the conditions of a row clause leaves the clause unchanged.
• rowClause_flip_change: a flip that changes a row clause changes its target condition in its own row or a gate condition on a labeled outgoing edge.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveChild_flip_same {k r : ℕ} {I : Type} (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) (a : I) : recursiveChild (flip x {((j, c), a)}) j c = flip (recursiveChild x j c) {a}

Flipping the raw coordinate ((j, c), a) flips coordinate a of the child at (j, c).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.recursiveChild_flip_other {k r : ℕ} {I : Type} (x : (Fin k × Fin r) × I → Bool) (j j' : Fin k) (c c' : Fin r) (a : I) (h : (j', c') ≠ (j, c)) : recursiveChild (flip x {((j, c), a)}) j' c' = recursiveChild x j' c'

Flipping the raw coordinate ((j, c), a) does not change the child at any position (j', c') ≠ (j, c).

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

Flipping ((j, c), a) does not change the clause of row i, provided it does not change the target value of the child at (j, c) when j = i, nor its gate value when T.Adj i j and c = label i j.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowClause_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 : 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) : 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)

If flipping ((j, c), a) changes the clause of row i, 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 the gate value of that child.