getD_of_compat_isSome'
plain-language theorem explainer
Known values in a partial assignment compatible with a total assignment must match the total assignment on those variables. Researchers deriving parity equalities for known bits under XOR constraints during SAT backpropagation cite this step. The proof uses case analysis on the option at the target variable, with compatibility forcing equality after ruling out the unknown case.
Claim. Let $n$ be a natural number, $σ : Var(n) → Option(Bool)$ a partial assignment, $a : Var(n) → Bool$ a total assignment, and $w : Var(n)$ a variable. If $σ$ is compatible with $a$ (i.e., $∀ v, σ(v) = some(a(v)) ∨ σ(v) = none$) and $σ(w)$ is defined, then getD($σ(w)$, false) = $a(w)$.
background
In this module partial assignments are functions from variables to Option Bool, where none marks an unknown bit and some b marks a determined value. Compatibility of $σ$ with a total assignment $a$ is the proposition that $σ$ agrees with $a$ wherever $σ$ is defined: for every variable $v$, either $σ(v) = some(a(v))$ or $σ(v) = none$. The module treats these objects as the state for backward propagation over CNF formulas that also contain XOR constraints. The lemma depends on the upstream definitions of compatible, the two Assignment types (Fin n → Bool), and Var as Fin n.
proof idea
The term proof begins with cases on the hypothesis $h : σ w$. The none branch yields an immediate contradiction with the isSome hypothesis after simp. The some b branch invokes compatibility at $w$, producing either an equality $b = a w$ or a none; the none disjunct is eliminated by simp, leaving the equality. Option.getD on some b then returns $b$, which equals $a w$ by the equality obtained from Option.some.injEq.
why it matters
The lemma supplies the value-extraction step required by the downstream knownParity_eq_parityOf_known' lemma, which equates the fold of known bits under XOR to the parity of the filtered known variables. It therefore supports the entire backpropagation machinery for SAT instances that mix clauses and parity constraints. No direct link exists to the T0-T8 forcing chain or the Recognition Composition Law; the result remains internal to the complexity encoding layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.