backprop_succeeds_from_PC
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that the PC condition holds for any concrete CNF or XOR system.
- Does not establish backpropagation success in the absence of the uniqueness hypothesis.
- Does not link the abstract step semantics to any concrete BPStep implementation.
- Does not address runtime or polynomial-time bounds on the propagation process.
formal statement (Lean)
208theorem backprop_succeeds_from_PC {n}
209 (inputs : Finset (Var n)) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n)
210 (_hpc : PC inputs aRef φ H)
211 (huniq : UniqueSolutionXOR { φ := φ, H := H }) :
proof body
Term-mode proof.
212 BackpropSucceeds φ H :=
213 backprop_succeeds_of_unique φ H huniq
214
215end SAT
216end Complexity
217end IndisputableMonolith