Formal Verification of Sen's Impossibility (Base Case n=2, m=4) in Lean 4 with DIMACS/LRAT Certificates

This archive provides a reproducible formalization of Sen’s “Impossibility of a Paretian Liberal” for the fixed base case with 2 voters and 4 alternatives (n=2, m=4). The result is verified in two independent layers: A pure Lean 4 proof of the base-case impossibility (UN ∧ MINLIB -> ¬SocialAcyclic), and A SAT certificate pipeline where a DIMACS CNF instance is proven UNSAT via an LRAT certificate, checked inside the Lean kernel. The repository includes: Lean source files for core definitions, axioms, and the base-case theorem, CNF/LRAT artifacts (sen24.cnf, sen24.lrat), a manifest and mechanical CNF audit tooling for schema/count consistency checks. Scope and limits: This release guarantees correctness for the fixed base case (n=2, m=4) under the definitions used in the repository. It does not claim a proof for general n,m or for alternative axiom formulations outside this encoding. Reproducibility: Build with lake build, (optional) regenerate and audit CNF with provided Python scripts, verify LRAT-backed UNSAT in Lean via the SAT module.