BackpropCompleteUnderInvariant
plain-language theorem explainer
BackpropCompleteUnderInvariant defines the implication that the isolation invariant on a CNF formula and XOR system guarantees backpropagation reaches a complete consistent state. Researchers establishing SAT completeness via backpropagation in the Recognition Science framework cite it as the Track B target. The declaration is a direct one-line encoding of the implication with no reduction steps.
Claim. Let $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR system. If the isolation invariant holds for $φ$ and $H$, then backpropagation succeeds: for every initial backpropagation state there exists a complete and consistent state satisfying $φ$ and $H$.
background
The module builds fully-determined backpropagation states from total assignments. CNF is a structure whose clauses field is a list of clauses over $n$ variables. XORSystem encodes parity constraints on those variables. IsolationInvariant is the structure requiring hasUnits (a variable with a singleton XOR constraint from $H$), connected (a propagation graph from which AllReachable reaches every variable), and noStalls (no configuration where unknowns remain but no rule applies). BackpropSucceeds is the proposition that every initial BPState reaches some complete consistent state. Upstream, BackpropSucceeds is defined by universal quantification over starting states to complete consistent ones, while IsolationInvariant captures the combinatorial conditions promised by geometric isolation.
proof idea
The definition is a direct statement of the implication IsolationInvariant n φ H → BackpropSucceeds φ H. It functions as a one-line wrapper with no lemmas or tactics applied.
why it matters
This definition is the explicit target for Track B completeness of backpropagation under isolation. It is referenced by the downstream lemma consistent_completeStateFrom, which shows states constructed from satisfying assignments remain consistent. The declaration advances the module goal of producing fully-determined states and links to the Recognition Science cost algebra via the shifted functional H and the propagation graph construction. The noStalls field remains open for Tseitin formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.