completeStateFrom

formal source

  11namespace SAT
  12
  13/-- Build a fully-determined backpropagation state from a total assignment. -/
  14def completeStateFrom {n} (x : Assignment n) : BPState n :=
  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