mem_zip_of_getElem'
plain-language theorem explainer
The declaration delivers a membership fact for zipped lists under bounded indexing. Researchers formalizing SAT backpropagation or clause evaluation in Lean would cite it for list manipulation lemmas. The proof goes through by rewriting membership to getElem form, checking the zipped length via simp and omega, then exhibiting the index witness directly.
Claim. Let $l_1 : List~α$, $l_2 : List~β$, and let $i : ℕ$ satisfy $i < |l_1|$ and $i < |l_2|$. Then $(l_1[i], l_2[i]) ∈ zip(l_1, l_2)$.
background
The module treats partial assignments for SAT backpropagation, where none denotes an unknown variable and some b a determined Boolean value. Clauses and XOR constraints are evaluated over these assignments, with backpropagation steps that identify the single unknown literal when the clause is satisfied. This lemma supplies a basic list fact used when indices must align across parallel structures such as literal lists and value lists of matching length.
proof idea
The tactic proof first rewrites the goal with List.mem_iff_getElem. It then proves the index lies inside the zipped list length by simp followed by omega. The final exact supplies the triple consisting of the original index, the length proof, and a reflexivity for the element equality.
why it matters
The lemma is invoked inside clauseUnit_correct, which proves that clauseUnit returns the correct Boolean value for a satisfying assignment when exactly one literal remains unknown. In the Recognition Science monolith this supports the correctness of backpropagation steps that appear in complexity arguments tied to the forcing chain and recognition composition law. No open scaffolding remains for this helper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.