Superquadratic sensitivity separation: recursive repair

Suppose the row clause i is false at x but becomes true after flipping the single raw bit ((j, c), a). Since the flip only affects the child (j, c), the clause had exactly one failed condition and the flip repairs it: either i is a target candidate, j = i, and the flip makes the final predicate accept the child (i, c), or i is a gate candidate, i → j is an edge with c = label i j, and the flip makes the gate predicate reject that child. This case analysis drives the zero-side sensitivity bounds.

Main results

• repaired_target_location: a target child rejected before a repairing flip is the flipped child.
• repaired_gate_location: a gate child accepted before a repairing flip is the flipped child.
• rowClause_repair_cases: a flip making a false row clause true repairs either its unique failed target or its unique failed gate.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.repaired_target_location {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 c' : Fin r) (a : I) (hf : rowClause T label F q (flip x {((j, c), a)}) i = true) (hz : F (Fin.last h) (recursiveChild x i c') = false) : (i, c') = (j, c)

If the row clause i holds after flipping the bit ((j, c), a) of x and the final predicate rejects the target child (i, c') of x, then (i, c') = (j, c).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.repaired_gate_location {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 j' : Fin k) (c : Fin r) (a : I) (hf : rowClause T label F q (flip x {((j, c), a)}) i = true) (hij' : T.Adj i j') (hon : F (gateIndex q) (recursiveChild x j' (label i j')) = true) : (j', label i j') = (j, c)

If the row clause i holds after flipping the bit ((j, c), a) of x and, along an edge i → j', the gate predicate accepts the child (j', label i j') of x, then (j', label i j') = (j, c).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rowClause_repair_cases {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) (hi : rowClause T label F q x i = false) (hf : rowClause T label F q (flip x {((j, c), a)}) i = true) : i ∈ targetCandidates T label F q x ∧ j = i ∧ F (Fin.last h) (recursiveChild x j c) = false ∧ F (Fin.last h) (flip (recursiveChild x j c) {a}) = true ∨ i ∈ gateCandidates T label F q x ∧ T.Adj i j ∧ c = label i j ∧ F (gateIndex q) (recursiveChild x j c) = true ∧ F (gateIndex q) (flip (recursiveChild x j c) {a}) = false

If the row clause i is false at x but true after flipping ((j, c), a), then either i is a target candidate, j = i, and the flip changes the final predicate on the child (j, c) from false to true; or i is a gate candidate, T.Adj i j, c = label i j, and the flip changes the gate predicate on the child (j, c) from true to false.