Updated: 2026-08-26
Formalized. The review surface covers every numbered definition, lemma, and theorem in the NeurIPS 2020 main paper and both named claims in its official supplement. All fourteen source presentations have transparent source-facing Lean statements. The ten result claims have checked proof endpoints; the four numbered definitions are reviewed directly as semantic declarations.
The formalization covers the finite pairwise-count likelihood model, MLE existence and uniqueness, Pareto efficiency, monotonicity, the impossibility of pairwise-majority consistency, and the impossibility of separability.
audit/library_semantic_review.json by terminal
closeout.FINAL_CLOSURE_RECEIPT.md is the canonical machine
closeout record after the terminal closeout transaction; this report is
the researcher-facing summary.The source is Ritesh Noothigattu, Dominik Peters, and Ariel D. Procaccia, Axioms for Learning from Pairwise Comparisons, NeurIPS 2020.
The audit uses a combined copy of the official proceedings paper and
official supplement (SHA-256
cbf69fcb0860f292056e7c8c3f1b7813b048877924ae6b6c037e84292d733163)
and its byte-pinned layout-preserving transcript. The source-only
inventory independently reconciles Lemmas 2.1–2.4; Definitions 3.1, 4.1,
5.1, and 6.1; Theorems 3.2, 4.2, 5.3, and 6.3; and supplementary Claims
A.1 and C.1.
Exact source spans, semantic context, and proof routes are in
audit/paper_statement_map.json. Source-facing Lean
statements are in PaperInterface.lean; paired proof
endpoints are in ProofInterface.lean.
| Result | Comparison with source |
|---|---|
| Lemma 2.1 | Exact. |
| Lemma 2.2 | Exact. |
| Lemma 2.3 | Quantifier corrected: positive directed counts only between distinct alternatives; the source sup-norm bound follows. Correction. |
| Lemma 2.4 | Exact. |
| Definitions 3.1, 4.1; Theorems 3.2, 4.2 | Exact. |
| Definition 5.1; Theorem 5.3 | Exact. |
| Definition 6.1; Theorem 6.3 | Exact. |
| Supplementary Claims A.1 and C.1 | Exact. |
None.
None.
Theorems 5.3 and 6.3 replace continuity of the maximizer with a compact likelihood gap and an exact rational perturbation under the source assumptions. Proof details.
The reusable library now includes finite pairwise-count datasets, comparison graphs, CDF-like pairwise links, fixed-reference MLEs, perfect-fit distances, likelihood existence and uniqueness tools, score-exchange lemmas, and exact counterexample constructions. These components are independent of the paper namespace and can support later ranking and preference-learning work.
Lemma 2.3’s positive-count premise ranges over distinct alternatives because diagonal counts are zero. The memo gives this local clarification.
None.
PaperInterface.lean presents fourteen source items: four semantic definitions and ten result claims. ProofInterface.lean supplies one exact-type endpoint for each result; the four definitions remain direct declarations rather than artificial theorem wrappers.
Assumptions.lean introduces no paper-local axiom. Four
graph-selected paper-model prerequisites have current matching judgments
in the paper-prerequisite ledger.
No material reusable-library prerequisite is selected.
The source map binds pairwise counts, comparison graph, link/CDF likelihood, finite MLE, perfect fit, score bounds, and the Pareto, monotonicity, majority-consistency, and separability formulas to their source presentations.
The reusable library contains the general pairwise-count dataset, graph, likelihood, link, MLE, perfect-fit, and comparison-axiom machinery. Paper numbering and explicit counterexample instances remain paper-local.
The dependency DAG places the model and supplementary claims before the main results and shows the four axiom results depending on the finite MLE foundation. The retained visual inspection found readable labels, correct arrow direction, and no clipping or node overlap.
The weak-order PMC definition and its Theorem 5.3 endpoint compile and pass bounded independent source comparison. Their current closeout evidence is being synchronized; the retained receipt describes its pinned prior tree.
Retained focused proof-interface and root builds passed. The current graph records ten matching direct result judgments and four matching paper-model prerequisites. The accepted graph and closure receipt bind the closeout surface; no new Lean or semantic review was run for this document edit.
The checked source definitions are the pairwise-comparison/MLE model, Definition 3.1 Pareto efficiency, Definition 4.1 monotonicity, Definition 5.1 pairwise-majority consistency, and Definition 6.1 separability.
The ten direct comparisons are in the source-to-Spec ledger; model premises are in the paper-prerequisite ledger, and source-proof fidelity records the counterexample proof replacement.
The source map inventories all fourteen named source presentations. The ten result rows have current matching direct judgments, and the four definition rows are covered as semantic model prerequisites. The accepted graph binds both groups without counting the definitions as extra theorem claims.