Sensitivity separation: recursive failures

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveFailures.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

def Complexity.BooleanAnalysis.Sensitivity.Internal.targetFailures {k r h : ℕ} {I : Type} (F : Fin (h + 1) → (I → Bool) → Bool) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) : Finset (Fin r)

The columns of a row whose target predicates reject.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.targetFailures F x i = {c : Fin r | F (Fin.last h) (Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveChild x i c) = false}

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.gateFailures {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 : Fin k) : Finset (Fin k)

Outgoing neighbors whose gate predicates accept, violating their row conditions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.targetCandidates {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) : Finset (Fin k)

Rows with exactly one failed target and no failed gate condition.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.gateCandidates {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) : Finset (Fin k)

Rows with no failed target and exactly one failed gate condition.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.targetWitness {k r h : ℕ} {I : Type} (F : Fin (h + 1) → (I → Bool) → Bool) (x : (Fin k × Fin r) × I → Bool) (hr : 0 < r) (i : Fin k) : Fin r

Choose a failed target column, with column zero as fallback.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.targetWitness F x hr i = if hi : (Complexity.BooleanAnalysis.Sensitivity.Internal.targetFailures F x i).Nonempty then Exists.choose hi else ⟨0, hr⟩

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.gateWitness {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 : Fin k) : Fin k

Choose a failed gate neighbor, with the row itself as fallback.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.targetFailures_empty_iff {k r h : ℕ} {I : Type} (F : Fin (h + 1) → (I → Bool) → Bool) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) : targetFailures F x i = ∅ ↔ ∀ (c : Fin r), F (Fin.last h) (recursiveChild x i c) = true

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateFailures_empty_iff {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 : Fin k) : gateFailures T label F q x i = ∅ ↔ ∀ (j : Fin k), T.Adj i j → F (gateIndex q) (recursiveChild x j (label i j)) = false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.targetFailures_singleton {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) (hr : 0 < r) (i : Fin k) (hi : i ∈ targetCandidates T label F q x) : targetFailures F x i = {targetWitness F x hr i}

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateFailures_singleton {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 : Fin k) (hi : i ∈ gateCandidates T label F q x) : gateFailures T label F q x i = {gateWitness T label F q x i}

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.targetCandidates_card {k r h : ℕ} {I : Type} (T : Tournament k) (A : GoodLabeling T r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (hr : 0 < r) : (targetCandidates T A.label F q x).card < 16

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateCandidates_neighbor {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i j : Fin k) (hi : i ∈ gateCandidates T label F q x) (hj : j ∈ gateCandidates T label F q x) (hij : T.Adj i j) : j = gateWitness T label F q x i

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateCandidates_card {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) : (gateCandidates T label F q x).card ≤ 3