complete
plain-language theorem explainer
A definition stating that a BPState over n variables is complete exactly when its partial assignment map returns a definite Boolean for every variable index. Researchers tracking progress in SAT backpropagation within the Recognition Science cost algebra cite this predicate to mark when a partial state becomes total. The definition is a direct universal quantification over the assignment component of BPState.
Claim. A state $s$ over $n$ variables is complete if and only if for every variable index $v$, the assignment at $v$ is defined (i.e., returns some Boolean value).
background
The module treats partial assignments for backpropagation, with none marking an unknown bit and some b a determined Boolean. BPState n is the structure whose sole field is assign : PartialAssignment n. The predicate complete is introduced immediately after the structure and before consistent, which requires a total assignment agreeing with the partial map on all known bits while satisfying a CNF and an XORSystem.
proof idea
One-line definition that directly encodes the condition that the assignment map returns isSome = true for every variable, using the structure field of BPState.
why it matters
The predicate supplies the completeness check used by downstream declarations including windowSums_shift_equivariant in CostAlgebra, potential_implies_exact in LedgerAlgebra, OctaveLoop in CoherenceTechnology, and rs_pattern in PhotobiomodulationDevice. It supports the backpropagation machinery that feeds into ledger algebra and applied coherence structures, aligning with the eight-tick octave and full determination steps in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.