clauseUnit_correct
plain-language theorem explainer
clauseUnit_correct establishes that if a partial assignment leaves exactly one literal unknown in clause C, all known literals evaluate false under a compatible full assignment a, and a satisfies C, then clauseUnit returns the pair (v, b) with b matching a(v). Researchers building backpropagation SAT solvers or verifying complexity reductions in Recognition Science cite it for propagation soundness. The proof filters the unknown list to a singleton, shows the satisfying literal must be that unknown entry, and performs polarity case analysis to
Claim. Let $n$ be a natural number, let $σ$ be a partial assignment over $n$ variables, let $a$ be a full assignment compatible with $σ$, let $C$ be a clause satisfied by $a$, and suppose clauseUnit$(σ, C)$ returns some pair $(v, b)$. Then $b = a(v)$.
background
PartialAssignment $n$ is the type Var $n$ → Option Bool, where none marks an undetermined variable and some $b$ records a fixed Boolean value. Clause $n$ is a structure holding a list of at most three literals, each a pair (variable index, polarity). The clauseUnit function maps a partial assignment and clause to an optional (variable, Boolean) pair precisely when exactly one literal remains unknown and every known literal is false under the assignment.
proof idea
The tactic proof unfolds clauseUnit, splits on the length of the filtered unknown list equaling one, obtains the singleton element via singleton_eq_get_zero', proves all known literals are false using known_lit_false'', extracts the satisfying literal from the assumption evalClause $a$ $C$ = true, shows that literal must be the unknown entry, and finishes by case analysis on the literal's polarity (pos or neg) to equate $b$ with $a(v)$ or its negation.
why it matters
The result supplies the key correctness step for unit propagation inside the backpropagation module and is invoked by bp_step_sound to preserve compatibility after each step. It replaces a former axiom, completing the deterministic justification that clauseUnit recovers the correct value from any satisfying assignment. The lemma sits in the Complexity.SAT layer that supports the broader Recognition Science reduction of satisfiability questions to the phi-ladder and eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.