singleton_eq_get_zero'
plain-language theorem explainer
If a list has length exactly one then it equals the singleton containing its sole element, recovered by indexing at position zero. SAT backpropagation code cites this helper when a clause reduces to a single undetermined literal. The argument proceeds by exhaustive structural case analysis on the list.
Claim. Let $l$ be a list whose length equals one. Then there exists an element $x$ such that $l=[x]$ and $x$ equals the element of $l$ at index zero.
background
The module treats partial assignments for backpropagation in SAT instances, marking variables unknown by none and determined by some Boolean. Unit clauses arise when exactly one literal remains undetermined, triggering extraction of that literal. The lemma supplies the required list-identity fact for this extraction step.
proof idea
The term proof matches on the list structure. Empty and length-two-or-more cases are discharged by simp against the length hypothesis; the singleton case returns the witness and the two equalities by reflexivity.
why it matters
clauseUnit_correct invokes the lemma to confirm that the value returned by clauseUnit matches the satisfying assignment. The result therefore supports the inductive step that backpropagation preserves satisfiability inside the Recognition Science encoding of SAT complexity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.