BackpropCompleteUnderInvariant

formal source

  88  noStalls : ∀ s : BPState n, ¬complete s → ∃ s', BPStep φ H s s' ∧ s ≠ s'
  89
  90/-- Backprop completeness under the isolation invariant (Track B target). -/
  91def BackpropCompleteUnderInvariant {n} (φ : CNF n) (H : XORSystem n) : Prop :=
  92  IsolationInvariant n φ H → BackpropSucceeds φ H
  93
  94/-- **PROVED**: Determined values match the unique solution.
  95
  96**Proof**: Pick x to be the unique solution (from `huniq`).
  97Then if all determined values in s match x, the premise `s.assign v = some (x v)`
  98combined with `hdetermined : s.assign v = some b` gives `b = x v`.
  99
 100**Status**: PROVED (formerly axiom) -/
 101theorem determined_values_correct {n} (φ : CNF n) (H : XORSystem n)
 102    (huniq : UniqueSolutionXOR { φ := φ, H := H })
 103    (s : BPState n) (v : Var n) (b : Bool)
 104    (hdetermined : s.assign v = some b) :
 105    ∃ x : Assignment n, (∀ v', s.assign v' = some (x v')) →
 106      evalCNF x φ = true ∧ satisfiesSystem x H ∧ x v = b := by
 107  -- UniqueSolutionXOR means ∃! a, evalCNF a φ = true ∧ satisfiesSystem a H
 108  unfold UniqueSolutionXOR at huniq
 109  -- Get the unique solution
 110  obtain ⟨x, ⟨hx_sat_φ, hx_sat_H⟩, _⟩ := huniq
 111  -- Use x as our witness
 112  use x
 113  intro h_all_match
 114  -- From h_all_match at v: s.assign v = some (x v)
 115  -- Combined with hdetermined: s.assign v = some b
 116  -- We get: b = x v
 117  have hv_match := h_all_match v
 118  rw [hdetermined] at hv_match
 119  simp only [Option.some.injEq] at hv_match
 120  exact ⟨hx_sat_φ, hx_sat_H, hv_match.symm⟩
 121