determined_values_correct

formal source

  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
 122/-- **FALSIFIED HYPOTHESIS**: Geometric propagation theorem.
 123
 124    Original claim: geometric isolation enables propagation completeness.
 125
 126    **FALSIFICATION (2026-04-07):**
 127    The `IsolationInvariant.noStalls` condition requires that BPStep (unit
 128    propagation + XOR inference) never stalls on any incomplete state.
 129    This is provably false:
 130
 131    Counterexample — Tseitin formulas on expander graphs: