complete_completeStateFrom
plain-language theorem explainer
The lemma shows that any total Boolean assignment to n variables induces a complete backpropagation state in which every variable receives a definite value. SAT backpropagation researchers cite it to confirm that satisfying assignments produce fully determined states for propagation. The proof proceeds by a direct term-mode verification that the constructed state satisfies the completeness predicate by reflexivity on each variable.
Claim. Let $x$ be a total assignment of Boolean values to $n$ variables. Let $s$ be the backpropagation state defined by $s(v) := x(v)$ for every variable $v$. Then $s$ is complete: every variable is assigned a definite value.
background
An assignment is a function from the set of $n$ variables to Boolean values. The construction completeStateFrom turns such an assignment into a backpropagation state by mapping every variable to a definite (Some) value. The predicate complete on a state holds exactly when the assignment map returns a defined value for every variable.
proof idea
The proof is a one-line term-mode wrapper. It introduces an arbitrary variable $v$ and applies reflexivity, which holds directly from the definition of the constructed state.
why it matters
This result supplies the completeness component for the theorem backprop_succeeds_of_unique, which shows backpropagation recovers a solution when a unique satisfying assignment exists under XOR constraints. It closes one half of the semantic existence argument inside the SAT completeness module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.