Mapping the SAT/UNSAT Frontier of Sen’s Liberal Paradox at n=2, m=4: An Auditable Possibility Atlas with Proof- and Witness-Carrying Evidence

抄録

Classical impossibility theorems identify infeasible axiom sets, but they do not by themselves answer the engineering question of which lever changes restore feasibility or what evidence should be trusted when that search is automated. We address this question by constructing an auditable possibility atlas for a fixed finite instance of Sen’s impossibility of a Paretian liberal (sen24, n = 2, m = 4). Across 32 axiom configurations induced by five levers, the atlas records which combinations are SAT or UNSAT and ties each outcome to replayable evidence. It identifies the sen24 SAT/UNSAT frontier, explains boundary UNSAT cases by one MUS and one small MCS candidate, and turns relaxed SAT cases into validated rule examples through deterministic gallery and rule-card artifacts. Beyond this local boundary explanation stage, a stronger repair stage reports full repair enumeration and checks it by triangulation against an independent optimum baseline.The contribution is therefore not SAT solving in social choice per se, but an auditableworkflow around atlas artifacts with an explicit proof/audit/witness split. The committedsen24 semantic theorem and a committed LRAT replay are checked in Lean; CNF schemaconformance, manifest linkage, and clause-family accounting are mechanically audited;reported SAT models are witness-validated against concrete CNF instances; and the short-cycle encoding used for rationality is connected to acyclicity only by a sen24-specific finite Python check. The repository packages commands, hashes, metadata, and paper-facing artifacts into a reproducible evidence bundle, so that the frontier, its boundary explanations, the stronger repair outputs, and the SAT witness examples can be regenerated and audited without trusting solver output alone.