determined_values_correct
Determined values in a partial assignment must match the unique solution when a CNF formula and XOR system admit exactly one satisfying assignment. Researchers studying propagation-based SAT solvers would cite this to confirm that backpropagation steps preserve correctness. The proof extracts the unique solution from the uniqueness hypothesis, uses it as witness, and matches the determined bit by direct equality after rewriting.
claimLet $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR constraint system on the same variables. Suppose there is a unique total assignment $x$ such that $φ$ evaluates to true under $x$ and $x$ satisfies $H$. For any backpropagation state $s$, variable $v$, and boolean $b$ where $s$ has determined $v$ to $b$, there exists an assignment $x$ such that every determined value in $s$ agrees with $x$, $x$ satisfies both $φ$ and $H$, and $x(v) = b$.
background
A backpropagation state consists of a partial assignment to variables together with CNF and XOR constraints. An assignment is a total function from the $n$ variables to booleans. UniqueSolutionXOR encodes the existence of exactly one total assignment that satisfies the CNF evaluation predicate and the XOR system simultaneously. The module focuses on constructing fully-determined backpropagation states from total assignments. Upstream results supply the BPState structure for partial assignments and the CNF evaluation and satisfaction predicates.
proof idea
The tactic proof first unfolds the UniqueSolutionXOR hypothesis. It obtains the unique satisfying assignment $x$ via obtain and uses it as the existential witness. The assumption that all determined values in the state match $x$ is applied at the specific variable $v$. Rewriting the determination hypothesis into this matching fact, followed by simplification on the option equality, yields that $b$ equals $x(v)$. The three required conjuncts then follow immediately.
why it matters in Recognition Science
The theorem supplies a key correctness invariant for backpropagation under uniqueness assumptions inside the SAT completeness development. It replaces an earlier axiom and ensures that any value fixed by propagation steps coincides with the global solution. The surrounding module explores isolation and propagation for 3SAT, though related geometric isolation hypotheses have been falsified on expander graphs. No downstream uses are recorded yet.
scope and limits
- Does not prove existence or uniqueness of a solution.
- Does not apply when the instance has multiple or zero solutions.
- Does not bound the number of propagation steps required.
- Does not address satisfiability of arbitrary CNF-XOR instances.
formal statement (Lean)
101theorem determined_values_correct {n} (φ : CNF n) (H : XORSystem n)
102 (huniq : UniqueSolutionXOR { φ := φ, H := H })
proof body
Tactic-mode proof.
103 (s : BPState n) (v : Var n) (b : Bool)
104 (hdetermined : s.assign v = some b) :
105 ∃ x : Assignment n, (∀ v', s.assign v' = some (x v')) →
106 evalCNF x φ = true ∧ satisfiesSystem x H ∧ x v = b := by
107 -- UniqueSolutionXOR means ∃! a, evalCNF a φ = true ∧ satisfiesSystem a H
108 unfold UniqueSolutionXOR at huniq
109 -- Get the unique solution
110 obtain ⟨x, ⟨hx_sat_φ, hx_sat_H⟩, _⟩ := huniq
111 -- Use x as our witness
112 use x
113 intro h_all_match
114 -- From h_all_match at v: s.assign v = some (x v)
115 -- Combined with hdetermined: s.assign v = some b
116 -- We get: b = x v
117 have hv_match := h_all_match v
118 rw [hdetermined] at hv_match
119 simp only [Option.some.injEq] at hv_match
120 exact ⟨hx_sat_φ, hx_sat_H, hv_match.symm⟩
121
122/-- **FALSIFIED HYPOTHESIS**: Geometric propagation theorem.
123
124 Original claim: geometric isolation enables propagation completeness.
125
126 **FALSIFICATION (2026-04-07):**
127 The `IsolationInvariant.noStalls` condition requires that BPStep (unit
128 propagation + XOR inference) never stalls on any incomplete state.
129 This is provably false:
130
131 Counterexample — Tseitin formulas on expander graphs:
132 • At the initial empty state, every 3-clause has 3 unknown literals → no unit clause.
133 • XOR constraints span many variables → no single-unknown XOR constraint.
134 • BPStep cannot fire, yet the state is incomplete → noStalls is violated.
135 • Ben-Sasson & Wigderson (2001) proved expander-Tseitin formulas require
136 exponential-length resolution proofs; no local propagation suffices.
137
138 Additionally, SAT has no intrinsic geometric structure — variables can be
139 permuted arbitrarily — so Morton ordering provides zero structural advantage.
140
141 **STATUS**: FALSIFIED — `IsolationInvariant.noStalls` is unsatisfiable for
142 expander-based formulas regardless of XOR system choice. -/