BackpropSucceeds
plain-language theorem explainer
Backpropagation succeeds for CNF formula phi and XOR system H when every initial partial-assignment state reaches some complete state that satisfies both. Researchers working on SAT completeness in the Recognition Science setting cite this predicate when proving algorithmic reachability from uniqueness or isolation invariants. The declaration is a direct definition that packages the universal-existential statement without further proof obligations.
Claim. For a CNF formula $phi$ over $n$ variables and an XOR constraint system $H$, backpropagation succeeds if for every initial state $s_0$ (a partial assignment), there exists a state $s$ such that $s$ is complete (every variable assigned) and consistent, i.e., there is a total assignment agreeing with $s$ on known values that evaluates $phi$ to true and satisfies $H$.
background
BPState packages a partial assignment over $n$ variables, where each entry is either unknown or fixed to a boolean. The complete predicate requires every variable to carry a definite value. The consistent predicate asserts existence of a total assignment that matches the partial one on determined bits, satisfies all clauses of $phi$, and meets every parity constraint in $H$ (the XORSystem).
proof idea
Direct definition of the success predicate. It expands to a universal quantifier over all BPStates followed by an existential claim that a complete consistent state exists, without invoking any transition lemmas or tactics.
why it matters
This predicate is the target property in downstream completeness statements. It appears in BackpropCompleteUnderInvariant (which adds an isolation invariant), in backprop_succeeds_from_PC (which derives success from propagation completeness plus uniqueness), and in backprop_succeeds_of_unique (which shows a unique solution under XOR constraints suffices). Within Recognition Science it links semantic satisfiability of CNF plus XOR constraints to the existence of a terminating backpropagation path, supporting the broader forcing-chain and uniqueness results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.