Sensitivity separation: recursive flips #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveFlips.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.
theorem
Complexity.BooleanAnalysis.Sensitivity.Internal.rowClause_eq_of_conditions
{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 y : (Fin k × Fin r) × I → Bool)
(i : Fin k)
(ht : ∀ (c : Fin r), F (Fin.last h) (recursiveChild x i c) = F (Fin.last h) (recursiveChild y i c))
(hg :
∀ (j : Fin k),
T.Adj i j → F (gateIndex q) (recursiveChild x j (label i j)) = F (gateIndex q) (recursiveChild y j (label i j)))
:
theorem
Complexity.BooleanAnalysis.Sensitivity.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))
:
theorem
Complexity.BooleanAnalysis.Sensitivity.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)
: