determined_values_correct
plain-language theorem explainer
determined_values_correct establishes that any value fixed in a backpropagation state must coincide with the unique satisfying assignment of a CNF formula together with an XOR system. Researchers developing propagation-based SAT solvers under uniqueness assumptions would cite the result to guarantee consistency of partial determinations. The tactic proof extracts the unique solution from the uniqueness hypothesis and equates the determined bit to the solution bit via option equality.
Claim. Let $φ$ be a CNF formula on $n$ variables and $H$ an XOR constraint system. If there is a unique assignment satisfying both $φ$ and $H$, and if a backpropagation state $s$ has fixed variable $v$ to boolean $b$, then there exists an assignment $x$ such that every determined entry in $s$ matches the corresponding value of $x$, $x$ satisfies $φ$ and $H$, and $x(v)=b$.
background
The module develops constructions that turn total assignments into fully-determined backpropagation states. BPState is a structure holding a partial assignment over the $n$ variables. UniqueSolutionXOR asserts existence of exactly one total assignment that satisfies both the CNF formula (via evalCNF) and the XOR system (via satisfiesSystem). Assignment is the type of total maps from variables to booleans; CNF and XORSystem are the respective constraint collections.
proof idea
The tactic proof unfolds UniqueSolutionXOR to obtain the unique satisfying assignment $x$. It supplies $x$ as the existential witness. The universal assumption that all determined values in the state match $x$, together with the concrete determination $s.assign v = some b$, yields $b = x v$ by rewriting and simplification on Option.some.injEq.
why it matters
The declaration discharges a former axiom inside the SAT completeness development by proving determined values are forced by the unique solution. It supports the module goal of building complete states from total assignments under uniqueness. The surrounding file records that a related geometric isolation hypothesis has been falsified for expander-based Tseitin formulas, since unit propagation and XOR inference stall on incomplete states. The result does not invoke the Recognition Science forcing chain or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.