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
proof body
Term-mode proof.
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. 55-/ 56 57/-- Propagation graph: variable v₁ → v₂ if determining v₁ can force v₂. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.