consistent_completeStateFrom

formal source

  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:
  49- Linear masks target every variable via single-variable constraints H_{a,n,j}
  50- XOR cascade: determined variables unlock others via parity relations
  51- Clause cascade: known values simplify clauses, forcing more variables
  52- Termination: geometric structure ensures no stalls
  53
  54Formal verification is in progress via Tracks A and B.