backprop_succeeds_of_unique
If a CNF formula over n variables paired with an XOR system admits a unique satisfying assignment, then backpropagation reaches a complete consistent state from every initial BPState. Researchers modeling constraint propagation or SAT completeness in algebraic frameworks cite this for its semantic guarantee that uniqueness alone forces termination. The proof extracts the unique assignment, builds the target state directly from it, and invokes two supporting lemmas on completeness and consistency.
claimLet $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR system on those variables. If the pair $(φ, H)$ has a unique solution, then backpropagation succeeds: for every initial backpropagation state $s_0$, there exists a state $s$ that is both complete and consistent with $φ$ and $H$.
background
The module constructs fully-determined backpropagation states from total assignments. A CNF is a conjunction of clauses over $n$ variables. BackpropSucceeds $φ$ $H$ asserts that every initial BPState reaches some state that is complete (every variable assigned) and consistent (satisfies all clauses in $φ$ and all XOR constraints in $H$).
proof idea
The tactic proof introduces an arbitrary starting state, destructures the uniqueness hypothesis to obtain the unique satisfying assignment $x$, then refines the goal to the state built by completeStateFrom $x$. It applies complete_completeStateFrom to discharge completeness and consistent_completeStateFrom (after splitting the satisfaction facts for $φ$ and $H$) to discharge consistency.
why it matters in Recognition Science
This theorem supplies the uniqueness-to-success direction used by backprop_succeeds_from_PC, which states that PC inputs imply BackpropSucceeds via uniqueness. It closes the semantic existence half of the SAT completeness argument without requiring a concrete BPStep relation. The result sits inside the broader Recognition Science effort to derive computational structure from the same algebraic primitives (J-cost, RCL) that generate the physical constants.
scope and limits
- Does not prove that any given CNF and XOR system possesses a unique solution.
- Does not connect uniqueness to a concrete cellular-automaton step rule.
- Does not bound the number of backpropagation steps required.
- Does not address satisfiability when multiple solutions exist.
Lean usage
theorem backprop_succeeds_from_PC {n} (inputs : Finset (Var n)) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) (_hpc : PC inputs aRef φ H) (huniq : UniqueSolutionXOR { φ := φ, H := H }) : BackpropSucceeds φ H := backprop_succeeds_of_unique φ H huniqformal statement (Lean)
195theorem backprop_succeeds_of_unique {n} (φ : CNF n) (H : XORSystem n)
196 (huniq : UniqueSolutionXOR { φ := φ, H := H }) :
proof body
Tactic-mode proof.
197 BackpropSucceeds φ H := by
198 intro s0
199 rcases huniq with ⟨x, hx, _uniq⟩
200 refine ⟨completeStateFrom x, ?hcomp, ?hcons⟩
201 · exact complete_completeStateFrom x
202 · rcases hx with ⟨hxφ, hxH⟩
203 exact consistent_completeStateFrom x φ H hxφ hxH
204
205/-- PC ⇒ backpropagation succeeds (via uniqueness).
206Note: with the current abstract step semantics, uniqueness alone suffices for success.
207PC becomes relevant once a concrete BPStep is connected to semantic forcing. -/