list_singleton_of_length_one'
Any list of length exactly one equals the singleton containing its element at index zero. This helper supports extraction of the unique unknown variable inside xorMissing for XOR constraints under partial assignments. The proof proceeds by exhaustive case analysis on list constructors, with the length hypothesis eliminating the empty and longer cases via simplification.
claimLet $l$ be a list over a type $A$ such that the length of $l$ equals 1. Then $l$ equals the singleton list whose sole element is the entry of $l$ at position zero.
background
The module treats partial assignments in which none marks an unknown variable and some b marks a determined Boolean value. In xorMissing, the variables of an XOR constraint are filtered to those whose values remain unknown under the partial assignment; the resulting list of unknowns is checked for length one before indexing. This lemma supplies the equality needed to equate that filtered list with its singleton form for safe extraction via get. Upstream, the xorMissing definition itself performs the length-one check and the initial indexing step that this lemma justifies. Module-level imports of unrelated list constants (plot families, kinship systems, ore classes) do not affect the list lemma.
proof idea
The term proof matches on the structure of the input list. The empty-list case yields a contradiction with the length hypothesis after simplification. The singleton case reduces directly to the required equality. The two-or-more-elements case again contradicts the length hypothesis after simplification.
why it matters in Recognition Science
The lemma is invoked inside the proof of xorMissing_correct, which establishes that the Boolean returned by xorMissing equals the value under any satisfying assignment. It therefore closes the indexing step required for the backpropagation procedure on XOR constraints. Within the Recognition framework the result contributes to the complexity module by guaranteeing deterministic extraction when exactly one variable remains undetermined, consistent with the uniqueness steps in the forcing chain.
scope and limits
- Does not apply to lists whose length differs from one.
- Does not supply extraction for lists of arbitrary length.
- Does not treat non-list collections or infinite sequences.
formal statement (Lean)
197private lemma list_singleton_of_length_one' {α : Type*} (l : List α) (h : l.length = 1) :
198 l = [l.get ⟨0, by omega⟩] := by
proof body
Term-mode proof.
199 match l with
200 | [] => simp at h
201 | [x] => simp
202 | _ :: _ :: _ => simp at h
203
204/-- **PROVED**: xorMissing produces the correct value for a satisfying assignment.
205 If exactly one variable v is unknown in XOR constraint X, and a satisfies X,
206 then the value returned by xorMissing equals a v.
207
208 **Mathematical justification**: XOR is linear over GF(2).
209 If ⊕_{w ∈ X.vars} a(w) = X.parity and we know all values except a(v),
210 then a(v) = X.parity ⊕ (⊕_{w ≠ v} a(w)).
211
212 **Status**: PROVED (formerly axiom) -/