Sensitivity separation: recursive definitions

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveDefinitions.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.recursiveChild {k r : ℕ} {I : Type} (x : (Fin k × Fin r) × I → Bool) (j : Fin k) (c : Fin r) : I → Bool

Restrict a recursive input to one row and column of child coordinates.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveChild x j c a = x ((j, c), a)

def Complexity.BooleanAnalysis.Sensitivity.Internal.gateIndex {h : ℕ} (q : Fin h) : Fin (h + 1)

The reversed gate index among all indices except the final target index.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.gateIndex q = q.rev.castSucc

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateIndex_lt_last {h : ℕ} (q : Fin h) : gateIndex q < Fin.last h

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateIndex_antitone {h : ℕ} {q q' : Fin h} (hqq : q ≤ q') : gateIndex q' ≤ gateIndex q

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateIndex_strictAnti {h : ℕ} {q q' : Fin h} (hqq : q < q') : gateIndex q' < gateIndex q

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.rowClause {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) : Bool

A clause uses every target in its own row and one labeled gate per outgoing edge.

Equations

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

noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveFamily {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) : Bool

The next-level predicate is the disjunction of the literal row clauses.

Equations

• Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveFamily T label F q x = decide (∃ (i : Fin k), Complexity.BooleanAnalysis.Sensitivity.Internal.rowClause T label F q x i = true)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowClause_eq_true_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) : rowClause T label F q x i = true ↔ (∀ (c : Fin r), F (Fin.last h) (recursiveChild x i c) = true) ∧ ∀ (j : Fin k), T.Adj i j → F (gateIndex q) (recursiveChild x j (label i j)) = false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveFamily_eq_true_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) : recursiveFamily T label F q x = true ↔ ∃ (i : Fin k), rowClause T label F q x i = true

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveFamily_eq_false_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) : recursiveFamily T label F q x = false ↔ ∀ (i : Fin k), rowClause T label F q x i = false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.rowClause_nested {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 q' : Fin h} (hqq : q ≤ q') (x : (Fin k × Fin r) × I → Bool) (i : Fin k) (hi : rowClause T label F q' x i = true) : rowClause T label F q x i = true

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveFamily_nested {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) : NestedFamily (recursiveFamily T label F)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursiveFamily_zero {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hr : 0 < r) (hzero : ∀ (q : Fin (h + 1)), (F q fun (x : I) => false) = false) (q : Fin h) : (recursiveFamily T label F q fun (x : (Fin k × Fin r) × I) => false) = false

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.recursive_coordinates_card {k r : ℕ} {I : Type} [Fintype I] : Fintype.card ((Fin k × Fin r) × I) = k * r * Fintype.card I