pith. machine review for the scientific record. sign in
def definition def or abbrev high

complete

show as:
view Lean formalization →

A backpropagation state over n variables is complete when its assignment map returns a definite Boolean for every variable index. Researchers modeling SAT propagation or recognition-based constraint systems cite this predicate to mark full determination before evaluating clauses. The definition is a direct universal quantification over the assignment component of BPState.

claimLet $s$ be a backward-propagation state on $n$ variables whose assignment map returns an optional Boolean for each index. Then $s$ is complete if and only if the map yields a defined value for every variable.

background

The module treats partial assignments as the working state of constraint propagation on CNF formulas augmented by XOR systems. BPState is the structure that packages a PartialAssignment, where each entry is none (unknown) or some Boolean (determined). Completeness is the predicate that signals every variable has been fixed, enabling direct evaluation of the full formula and system. The sibling consistent predicate then requires that such a state agrees with a total assignment satisfying both the CNF and the XOR constraints. Upstream, the H reparametrization from CostAlgebra supplies the shifted cost $H(x)=J(x)+1$ used in semantic consistency checks.

proof idea

The definition is a one-line abbreviation that directly asserts the isSome predicate holds for every entry of the assignment map inside the given BPState. No lemmas or tactics are invoked; it serves as the primitive predicate consumed by consistent and by downstream propagation steps.

why it matters in Recognition Science

The predicate supplies the termination condition for backpropagation in the SAT encoding of recognition constraints. It is invoked by the consistent definition and appears in downstream results on octave loops, coherence patterns, and ledger algebra. Within the Recognition framework it closes the partial-to-total step that precedes evaluation against the phi-ladder and the eight-tick octave.

scope and limits

formal statement (Lean)

 105def complete {n} (s : BPState n) : Prop :=

proof body

Definition body.

 106  ∀ v, (s.assign v).isSome = true
 107
 108/-- Predicate: state is consistent with φ ∧ H (semantic notion). -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.