completeStateFrom
The definition constructs a fully determined BPState from a total assignment by wrapping each Boolean value in Some. Researchers proving that backpropagation succeeds for unique solutions under CNF and XOR constraints cite it to exhibit the terminal state. The construction is a direct record literal that populates the assign field without additional computation.
claimGiven a total assignment $x$ of $n$ Boolean variables, the map produces the BPState whose partial assignment satisfies $assign(v) = Some(x(v))$ for every variable $v$.
background
An Assignment n is a total function from the n variables to Bool. BPState n is the structure carrying a PartialAssignment n, where each entry may be None or Some b. The predicate complete on BPState requires that every variable entry is Some. These notions sit inside the SAT completeness development that combines CNF formulas with XOR systems; the definition supplies the terminal object needed when a unique satisfying assignment exists.
proof idea
The definition is a one-line record construction that sets the assign field to the function mapping each variable to Some of its value from the input assignment.
why it matters in Recognition Science
This definition supplies the complete state used in backprop_succeeds_of_unique to witness that backpropagation reaches a solution when a unique satisfying assignment exists. It also feeds the lemmas complete_completeStateFrom and consistent_completeStateFrom. In the Recognition framework it supports the reduction of constraint satisfaction to deterministic propagation steps.
scope and limits
- Does not verify consistency with the CNF or XOR system.
- Does not apply to partial assignments.
- Does not guarantee uniqueness of the resulting state.
Lean usage
refine ⟨completeStateFrom x, ?hcomp, ?hcons⟩formal statement (Lean)
14def completeStateFrom {n} (x : Assignment n) : BPState n :=
proof body
Definition body.
15 { assign := fun v => some (x v) }
16
17/-- The state built from a total assignment is complete. -/