IsolationInvariant
IsolationInvariant packages the three combinatorial conditions (unit XOR constraints, connected propagation graph, and non-stalling backpropagation steps) that geometric isolation is supposed to guarantee for a CNF formula and XOR system. Researchers analyzing SAT propagation completeness in the Recognition Science framework cite it when tracking backprop success under Track A invariants. It is introduced as a structure definition that directly encodes hasUnits, connected via AllReachable, and noStalls.
claimFor CNF formula $φ$ over $n$ variables and XOR system $H$, the isolation invariant holds if there exists variable $v$ and parity $p$ such that the unit constraint with those values belongs to $H$, there exists propagation graph $G$ and initial set such that AllReachable $G$ init holds, and for every incomplete BPState $s$ there exists a distinct successor $s'$ reachable by a BPStep rule.
background
BPState is a partial assignment over $n$ variables. BPStep is the inductive relation encoding single backpropagation rules (unit propagation and XOR pushing). The complete predicate holds precisely when every variable has a determined value. Upstream H from CostAlgebra is the shifted cost $H(x) = J(x) + 1$ satisfying the d'Alembert form of the Recognition Composition Law. The module constructs fully-determined states from total assignments and studies when backpropagation reaches them without stalls.
proof idea
This is a structure definition. It directly declares the three fields hasUnits (existence of a unit XOR), connected (existence of G and init with AllReachable), and noStalls (progress from every incomplete state via BPStep). No tactics or lemmas are applied; the declaration simply packages the properties.
why it matters in Recognition Science
It is the target invariant for geometric isolation and is used by BackpropCompleteUnderInvariant to link isolation to BackpropSucceeds. Downstream results include determined_values_correct (which assumes the invariant) and the falsified geometric_isolation_enables_propagation_hypothesis. The doc-comment explicitly warns that noStalls fails for Tseitin formulas on expander graphs, leaving open whether any geometric construction can inhabit the invariant for hard instances.
scope and limits
- Does not assert that the invariant is inhabited by any concrete formula.
- Does not construct the required units or graph from geometric properties.
- Does not guarantee satisfiability or completeness for expander graphs.
- Does not discharge the noStalls condition for Tseitin formulas.
formal statement (Lean)
82structure IsolationInvariant (n : Nat) (φ : CNF n) (H : XORSystem n) : Prop where
83 /-- At least one variable has a unit (single-variable) XOR constraint. -/
84 hasUnits : ∃ v : Var n, ∃ p : Bool, [{ vars := [v], parity := p }] ⊆ H
proof body
Definition body.
85 /-- The propagation graph constructed from φ ∧ H is connected. -/
86 connected : ∃ G : PropagationGraph n, ∃ init : Set (Var n), AllReachable G init
87 /-- No stall configurations: if unknowns remain, some rule applies. -/
88 noStalls : ∀ s : BPState n, ¬complete s → ∃ s', BPStep φ H s s' ∧ s ≠ s'
89
90/-- Backprop completeness under the isolation invariant (Track B target). -/