consistent_completeStateFrom
plain-language theorem explainer
The lemma shows that any assignment satisfying both a CNF formula and an XOR system produces a consistent complete backpropagation state. Researchers on SAT propagation completeness for geometrically isolated instances cite it when building determined states from known solutions. The proof is a direct term-mode construction packaging the input assignment with reflexivity and the given satisfaction facts.
Claim. Let $x$ be a Boolean assignment to $n$ variables, let $φ$ be a CNF formula, and let $H$ be an XOR system. If $x$ satisfies $φ$ and $H$, then the fully-determined backpropagation state built from $x$ is consistent with $φ$ and $H$.
background
An Assignment $n$ is a function Fin $n$ → Bool. A CNF $n$ consists of clauses, each a list of at most three literals. An XORSystem augments the formula with parity constraints. The function completeStateFrom constructs a fully-determined backpropagation state from a total assignment, per the module documentation. The predicate consistent verifies that the state satisfies the original formula and system without introducing contradictions.
proof idea
The proof is a one-line term-mode wrapper. It refines the consistent structure by supplying the original assignment, a reflexivity proof that all variables match, and the two satisfaction hypotheses.
why it matters
This lemma feeds the theorem backprop_succeeds_of_unique, which establishes that backpropagation succeeds under unique solutions for XOR-augmented instances. It supplies a basic existence step toward the module's main claim of propagation completeness for geometrically isolated SAT instances (Theorem 5). The surrounding module comment notes that linear masks and XOR cascades determine all variables, with formal verification still in progress via Tracks A and B.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.