An Auditable Possibility Atlas for Social Choice: Proof-/Witness-Carrying Evidence from the Sen24 Case Study

Impossibility theorems in social choice (Sen, Arrow) tell us that certain axiom combinations are infeasible — but they rarely tell us which combinations are feasible, or which relaxations open the door to possibility. We propose an auditable possibility atlas: a certified map over the axiom lever space that records, for each combination, whether a social choice rule exists (SAT) or not (UNSAT), together with replayable evidence for every verdict. Rather than claiming automated theorem discovery, we treat the atlas as an evidence-carrying artifact: Lean 4 fixes the semantic layer, LRAT proof certificates are kernel-checked, and SAT witnesses are independently validated. No verdict requires trusting the solver alone. As a first milestone, we construct the atlas for the Sen24 base case (n=2, m=4), identify the SAT/UNSAT boundary, extract MUS/MCS candidates for boundary cases, and present validated SAT rule examples. The scope is intentionally minimal — the goal is to establish the atlas methodology and trust model before scaling.