not_isSome_iff_isNone'
plain-language theorem explainer
The equivalence states that an Option value is absent precisely when it is explicitly None. It is cited inside clauseUnit_correct to manage unknown literals during SAT backpropagation over partial assignments. The proof is a one-line wrapper that splits on the Option constructor and simplifies both directions.
Claim. For any type $α$ and $o : Option α$, $¬(o.isSome) ↔ o.isNone$.
background
PartialAssignment n is the type Var n → Option Bool, with none marking an unknown variable and some b marking a determined value. The module develops backward propagation of satisfying assignments through CNF clauses and XOR constraints under such partial maps. This lemma supplies the basic Option equivalence that appears in filter and split steps inside clauseUnit_correct and related functions.
proof idea
One-line wrapper that applies the cases tactic to o and then invokes simp to discharge both directions of the biconditional.
why it matters
It is invoked by clauseUnit_correct, which proves that clauseUnit returns the correct Boolean for the unknown literal when a satisfies the clause. The result closes a small logical gap in the backpropagation correctness argument for SAT instances with partial information. No direct connection to the Recognition forcing chain or phi-ladder appears in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.