  15  { assign := fun v => some (x v) }
  16
  17/-- The state built from a total assignment is complete. -/
  18lemma complete_completeStateFrom {n} (x : Assignment n) :
  19    complete (completeStateFrom x) := by
  20  intro v
  21  rfl
  22
  23/-- The state built from a satisfying assignment is consistent. -/
  24lemma consistent_completeStateFrom {n} (x : Assignment n) (φ : CNF n) (H : XORSystem n)
  25    (hxφ : evalCNF x φ = true) (hxH : satisfiesSystem x H) :
  26    consistent (completeStateFrom x) φ H := by
  27  refine ⟨x, ?eqall, hxφ, hxH⟩
  28  intro v; rfl
  29
  30/-!
  31# Propagation Completeness for Geometrically Isolated SAT Instances
  32
  33This module defines the key theorems connecting geometric isolation to backward
  34propagation completeness. The main claim (Theorem 5 in the paper) is that for
  35every satisfiable 3-CNF φ, the isolating H ∈ 𝓗_geo(n) produces an instance
  36φ ∧ H where XOR-augmented propagation determines all variables.
  37
  38## Structure
  39
  401. `IsolationInvariant`: Structural conditions promised by geometric isolation
  412. `PropagationReachability`: Every variable is reachable by propagation chains
  423. `BackpropCompleteUnderInvariant`: Main implication
  434. `ProgramTarget`: Full end-to-end specification
  44
  45## Critical Claim Status
  46
  47The propagation-enablement theorem (Theorem 5) is the key claim requiring
  48verification. The proof strategy relies on:

papers checked against this theorem

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