  60
  61/-- A variable is reachable from initial units in the propagation graph.
  62    Defined inductively to ensure termination. -/
  63inductive Reachable {n} (G : PropagationGraph n) (init : Set (Var n)) : Var n → Prop
  64  | base : ∀ v, v ∈ init → Reachable G init v
  65  | step : ∀ u v, Reachable G init u → G.edges u v → Reachable G init v
  66
  67/-- All variables are reachable from initial units. -/
  68def AllReachable {n} (G : PropagationGraph n) (init : Set (Var n)) : Prop :=
  69  ∀ v, Reachable G init v
  70
  71/-- Structural invariant promised by the isolation construction (Track A).
  72
  73This captures the combinatorial conditions that geometric isolation guarantees:
  741. `hasUnits`: Some variables have unit constraints from H (direct determination)
  752. `connected`: The propagation graph reaches all variables from units
  763. `noStalls`: No stall configurations exist (propagation always has progress)
  77
  78**WARNING (2026-04-07)**: The `noStalls` field is UNSATISFIABLE for Tseitin formulas
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.