completeStateFrom
plain-language theorem explainer
This definition lifts a total Boolean assignment on n variables to a fully determined backpropagation state by wrapping each value in some. Researchers proving backpropagation success for unique XOR solutions cite it to supply explicit witness states. The construction is a direct record literal that populates the assign field without further computation.
Claim. Given a total assignment $x : Assignment(n)$, the state $completeStateFrom(x)$ is the $BPState(n)$ whose partial assignment sends every variable $v$ to $some(x(v))$.
background
The SAT completeness module works with CNF formulas augmented by XOR constraints. Assignment from RSatEncoding is the type $Fin n → Bool$, a total function assigning truth values to variables. BPState from Backprop is the structure containing a PartialAssignment field, and the predicate complete requires that every variable entry is $some$ rather than $none$.
proof idea
One-line definition that directly constructs the BPState record by setting assign to the lambda sending each v to some (x v).
why it matters
The definition supplies the witness state inside backprop_succeeds_of_unique, which concludes BackpropSucceeds under a UniqueSolutionXOR hypothesis. It is also the target of the supporting lemmas complete_completeStateFrom and consistent_completeStateFrom that verify the constructed state meets the completeness and consistency predicates. This construction therefore closes the semantic-to-algorithmic gap for existence arguments in the SAT backpropagation setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.