completeStateFrom
plain-language theorem explainer
completeStateFrom constructs a fully determined backpropagation state by lifting every entry of a total Boolean assignment into the Some constructor. Researchers proving SAT backpropagation completeness under unique solutions cite it to witness existence of a complete state from a known satisfying assignment. The definition is a direct one-line record construction with no lemmas or computation.
Claim. Given a total assignment $x$ of $n$ Boolean variables, the backpropagation state $s$ is defined by $s.assign(v) :=$ some$(x(v))$ for each variable $v$.
background
An Assignment is a total function from $n$ variables to Boolean values, as defined in RSatEncoding and CNF. BPState is the structure holding a partial assignment over those variables. The complete predicate on BPState requires every variable to be determined (isSome holds for all entries).
proof idea
The definition is a direct structural construction that embeds the input assignment function by wrapping each value in Some. No lemmas are invoked; it matches the BPState record exactly.
why it matters
It supplies the witness state in backprop_succeeds_of_unique for the semantic existence result under UniqueSolutionXOR. It also supports the supporting lemmas complete_completeStateFrom and consistent_completeStateFrom that verify the constructed state. The definition closes the constructive half of the backpropagation completeness argument in the SAT module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.