backprop_succeeds_of_unique

formal source

 192
 193/-- Backpropagation succeeds when there is a unique solution under XOR constraints.
 194This is a semantic existence result that does not rely on a specific step system. -/
 195theorem backprop_succeeds_of_unique {n} (φ : CNF n) (H : XORSystem n)
 196    (huniq : UniqueSolutionXOR { φ := φ, H := H }) :
 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. -/
 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 }) :
 212    BackpropSucceeds φ H :=
 213  backprop_succeeds_of_unique φ H huniq
 214
 215end SAT
 216end Complexity
 217end IndisputableMonolith