backprop_succeeds_from_PC
plain-language theorem explainer
If a CNF formula and XOR system have a unique solution and meet the PC condition for given inputs and reference assignment, then backpropagation succeeds on that pair. Researchers modeling SAT propagation or completeness in the Recognition Science setting would cite the result to separate uniqueness from concrete step semantics. The proof is a one-line term application of the uniqueness-implies-success lemma.
Claim. Let $n$ be a natural number, let $I$ be a finite set of variables, let $a$ be a total assignment to the $n$ variables, let $F$ be a CNF formula over those variables, and let $X$ be an XOR system over the same variables. If the PC condition holds for $I$, $a$, $F$, and $X$, and if the pair $(F,X)$ admits a unique solution, then every initial backpropagation state for $F$ and $X$ reaches a complete and consistent state.
background
The module constructs fully-determined backpropagation states from total assignments. CNF is the structure whose clauses are lists of literals over $n$ variables; Assignment is the type of total Boolean functions on those variables. BackpropSucceeds $F$ $X$ asserts that for every starting BPState there exists a later state that is both complete and consistent with respect to $F$ and $X$ (quoted from the upstream definition). PC is the hypothesis that the reference assignment and input set satisfy the propagation condition for the given formula and XOR system. The upstream lemma backprop_succeeds_of_unique states that uniqueness of the solution for the XOR system is already sufficient for the success property under the current abstract step semantics.
proof idea
The proof is a one-line term wrapper that applies the lemma backprop_succeeds_of_unique to the formula, the XOR system, and the uniqueness hypothesis. The PC hypothesis is carried but unused, consistent with the module note that uniqueness alone suffices until a concrete BPStep is linked to semantic forcing.
why it matters
The declaration isolates the role of uniqueness in the SAT completeness development and shows that the PC condition is not yet required under abstract semantics. It sits inside the broader effort to build complete states from total assignments and prepares the ground for later theorems that will connect concrete backpropagation steps. In the Recognition Science framework it echoes the T5 J-uniqueness step of the forcing chain, where a unique fixed point guarantees deterministic propagation. The open question it touches is the future attachment of a concrete BPStep to the semantic forcing relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.