Sensitivity separation: recursive repair

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveRepair.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.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)

theorem Complexity.BooleanAnalysis.Sensitivity.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)

theorem Complexity.BooleanAnalysis.Sensitivity.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