IsolationInvariant

formal source

  79on expander graphs (and many other hard formula families). At the initial empty
  80state, no clause is unit and no XOR constraint has a single unknown, so BPStep
  81cannot fire. This makes `IsolationInvariant` uninhabitable for such formulas. -/
  82structure IsolationInvariant (n : Nat) (φ : CNF n) (H : XORSystem n) : Prop where
  83  /-- At least one variable has a unit (single-variable) XOR constraint. -/
  84  hasUnits : ∃ v : Var n, ∃ p : Bool, [{ vars := [v], parity := p }] ⊆ H
  85  /-- The propagation graph constructed from φ ∧ H is connected. -/
  86  connected : ∃ G : PropagationGraph n, ∃ init : Set (Var n), AllReachable G init
  87  /-- No stall configurations: if unknowns remain, some rule applies. -/
  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