IsolationInvariant
plain-language theorem explainer
IsolationInvariant encodes three conditions on a CNF-XOR pair: existence of at least one unit XOR constraint, connectivity of the propagation graph from those units, and guaranteed progress under BPStep on every incomplete state. Researchers analyzing backpropagation completeness for SAT solvers cite it as the precise combinatorial target that geometric isolation must deliver. The declaration is a pure structure definition whose fields directly name the required properties with no further proof obligations.
Claim. Let $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR system. The isolation invariant holds when (i) there exists a variable $v$ and parity $p$ such that the singleton XOR constraint on $v$ with parity $p$ belongs to $H$, (ii) there exists a propagation graph $G$ and initial set of variables such that every variable is reachable from the initial set, and (iii) every incomplete back-propagation state admits a non-trivial BPStep transition.
background
BPState is the structure carrying a partial assignment during backward propagation; complete holds precisely when every variable has been assigned a value. BPStep is the inductive relation that fires unit-propagation or XOR-resolution rules to extend the assignment. AllReachable asserts that the propagation graph reaches every variable from a given seed set. The module constructs fully-determined states from total satisfying assignments and studies when backpropagation succeeds under isolation assumptions. Upstream, the shifted cost $H(x) = J(x) + 1$ satisfies the d'Alembert form of the recognition composition law, though the symbol $H$ here denotes the XOR constraint system rather than the cost function.
proof idea
The declaration is a structure definition whose three fields directly encode the invariant conditions. No lemmas are invoked and no tactics are executed; the definition serves as the interface type for subsequent statements that assume the invariant.
why it matters
IsolationInvariant is the hypothesis consumed by BackpropCompleteUnderInvariant and by the (now falsified) geometric_isolation_enables_propagation_hypothesis. It supplies the exact combinatorial promises that the isolation construction was intended to meet in the SAT-completeness track. The explicit warning in its documentation records that the noStalls field fails for Tseitin formulas on expander graphs, thereby closing one attempted route from geometric isolation to propagation completeness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.