Updated: 2026-09-06
The linear social-choice impossibilities and rule properties are proved on the stated selector domains, and Theorem 3.1 retains its source assumptions and conclusion.
The source is Luise Ge, Daniel Halpern, Evi Micha, Ariel D. Procaccia, Itai Shapira, Yevgeniy Vorobeychik, and Junlin Wu, Axioms for AI Alignment from Human Feedback, NeurIPS 2024.
The governing artifact is the published conference PDF and its paper-local, byte-pinned text extraction. The inventory covers the linear-ranking model; Definitions 2.1, 2.2, 4.1, 4.2, and C.1; the standard-loss, majority-loss, C1, LCPO, linear-Kemeny, Pareto-Kemeny, and leximax-plurality rule presentations; and every named result from Theorem 3.1 through Theorem C.6.
Exact source spans, semantic contexts, and Lean routes are in
audit/paper_statement_map.json. The result specifications
are in PaperInterface.lean; their proof endpoints are in
ProofInterface.lean.
| Result | Comparison with the paper |
|---|---|
| Definition 2.2; Lemmas 3.2–3.3; Theorems 3.6–3.7; Appendix B; Theorem C.4 | Exact. |
| Theorem 3.1, positive-input branch | Typo fixed: reverse the printed restricted-infimum sign; the impossibility conclusion is unchanged. |
| Lemmas 3.4–3.5 | Changed statements: a strict minimizer cone and closed-half-space objective gap replace the invalid weak-inclusion route; Theorem 3.1 is unchanged. |
| Footnote 7 witness | Typo fixed: parameter (delta,2)
replaces (1,1). |
| Theorem 4.3; Theorems C.2–C.3; Theorem C.6 | Restricted scope: fixed profile-independent tie keys. The broader selector claims remain unproved; necessity of fixed keys is unknown. |
| Theorem C.5 | Formalization gap: assume the source proof’s first-profile output. The reduction from every Pareto–Kemeny selector is unproved; necessity of that choice is unknown. |
Theorem C.5’s general-selector reduction remains unproved. Theorem 4.3 and Theorems C.2–C.3/C.6 retain their fixed-key selector scope; no proof or counterexample here settles the broader selector claims.
The strict-cone and closed-half-space arguments for Lemmas 3.4–3.5 do prove Theorem 3.1 with its original assumptions and conclusion.
The checked LCPO and leximax-plurality rule-level results use fixed, profile-independent tie keys selecting among source-eligible outcomes. A single-valued rule need not in general have such keys, so this is the stated scope of those formalized rule families, not an automatic consequence of being a function. Theorem C.5 instead retains the source proof’s local choice of its first-profile output as an explicit premise.
The source clarifications and corrections memo explains these scopes. It does not infer that the paper’s claims fail for other selectors merely because the current statements use these choices.
The memo gives the exact changes. Rule-selection restrictions are in Section 6.
The reusable library now supports finite feasible-ranking domains, linear reward parameters, Pareto and majority axioms, C1 rules, Kemeny disagreement, LCPO-style lexicographic selectors, and stable tie-broken rule families. The paper-local constructions retain their exact feature tables and profiles.
Footnote 7’s six-candidate ranking uses parameter
(delta,2) in place of (1,1); see the witness
note. Sections 6–7 cover the other statement scopes and proof
changes.
Section 7 explains the proof replacements and misplaced example attribution. Section 6 states the rule-selection scope; Section 10 links the exact local corrections.
PaperInterface.lean exposes fifteen transparent result contracts: Definition 2.2 with its consequences, the main-text theorem chain, the Appendix-B construction, and Theorems C.2–C.6. ProofInterface.lean supplies one exact-type proof endpoint for each. Other numbered definitions and rule presentations route through their semantic declarations.
Assumptions.lean introduces no paper-local axiom. Eight
material paper-local and twenty-one reusable-library prerequisites
selected by the Lean graph have current matching source-connected
judgments in the paper and library ledgers.
The source map binds the feature tables, linear losses, majority and Pareto conditions, Kemeny disagreement, LCPO, Pareto-Kemeny, and leximax-plurality formulas to the source. Lemmas 3.4–3.5 use documented corrected targets in the clarification memo.
Reusable components include rankings and profiles, finite linear reward models, feasible rankings, Pareto and majority axioms, C1 rules, Kemeny disagreement and selectors, LCPO, Pareto-Kemeny, and leximax-plurality. The loss-specific optimizers, source feature tables, and finite counterexamples remain paper-local.
The dependency DAG shows the Lemma 3.2–3.5 route to Theorem 3.1, keeps attached prose with Definition 2.2 and Theorem 3.7, and separates Appendix B and the Appendix-C rules. The retained visual inspection found readable labels, correct arrow direction, and no obscuring overlap.
The accepted graph binds fifteen direct judgments, of which twelve match the source literally and three match documented corrected targets, together with eight paper and twenty-one library prerequisite matches. Retained focused interface/root builds passed. See the accepted graph and closure receipt; no new semantic review was run.
Checked definitions include the linear-ranking model; Definitions 2.1, 2.2, 4.1, 4.2, and C.1; and the standard-loss, majority-loss, C1, LCPO, linear-Kemeny, Pareto-Kemeny, and leximax-plurality rule presentations.
The source-to-Spec ledger records the fifteen direct comparisons. Premise judgments are in the paper and library ledgers, and source-proof fidelity records the corrected-source routes.
The source map inventories the governing model, definitions, rule presentations, named results, and attached prose bundles. Every selected result has a direct current judgment, and the accepted graph binds the current source, interface, proof, and prerequisite evidence.