Updated: 2026-09-06
The formalization covers ordered-tier design invariance, pairwise and aggregate convergence results, randomized approval rules, the Mallows special case, and the exact dynamic program for two candidates’ joint locations. The dynamic program has a degree-six bound on arithmetic operations in its stated unit-cost model.
Propositions 2 and 4 include their finite-sample bounds. The source clarifications record the one-sided score-gap cases that make their rate conventions explicit.
The canonical pinned source is arXiv:1906.08160 / HCOMP 2019:
cited publication, SHA-256
667a8fb232a00e9161afc05cc6b68b3d8d950372531400e779388941fa68d41a;cited publication, SHA-256
be8a698dbe73835afaf8cd6079c7fc6a6a566fcaef25fc948c1e9be23771af32.The independent source inventory covers the finite ranking model, all three definitions, all nine named theoretical results, displayed probability and rate formulas, appendix proof steps, fixed mathematical examples, and the advertised Mallows joint-location algorithm. Raw datasets, fitted empirical estimates, figure pixels, and qualitative deployment recommendations are not mathematical theorem targets. The Durham numerical comparison is nevertheless checked exactly from the printed thousandths because it supports a source mathematical claim.
| Result | Comparison with source |
|---|---|
| Definitions 1–3 | Exact. |
| Proposition 1 | Exact. |
| Proposition 2 | Exact. |
| Proposition 3 | Exact. |
| Proposition 4 | Exact. |
| Theorems 1–2; Mallows corollary | Exact. |
| W-selection, Durham, and high-noise examples | Exact. |
| Joint-location dynamic program | Exact. |
None.
None.
None.
PMF.bind process rather than proving a recurrence
equal to itself.Option (Fin N) locations so
the same state type covers prefixes before and after each tracked
insertion.card (Option (Fin N) x Option (Fin N)) = (N+1)^2 then
yields the explicit N^2 (N+1)^4 <= (N+1)^6 bound.The dynamic-program layer is source-independent enough to be a candidate for future extraction into the reusable Mallows library. A sparse table over only reachable states should improve the dense degree-six count, but no stronger runtime theorem is claimed here. A separate rational or floating-point implementation could connect exact semantics to executable numerical plots; that would be an engineering extension rather than an unproved paper endpoint.
None.
No source-theorem correction is claimed. The source’s word “efficient” is made precise by a degree-six dense arithmetic-operation bound for the exact joint-location recurrence. Proposition 1 uses the source’s uniform random tie rule, including equality cases; it does not add a generic no-ties condition.
The source-curated inventory retains 66 mathematical items. The current selected source map retains 15 result contracts. Current review records cover the selected statements and their governing definitions. Definitions and algorithms are reviewed through their actual predicates, functions, and execution rules.
The source map connects the exact source passages to the expanded statements and models. Each selected result has a separate proof endpoint; the typed Lean graph checks its dependencies and axiom closure. Section 20 links the current review ledgers.
The selected models expose score and probability laws, randomized weights, ordered nonempty tiers, Mallows parameters, and valid approval cutoffs. These source conditions are carried by the actual semantic prerequisites; no algorithm-correctness conclusion is assumed.
The selected rate results retain the Chernoff expressions and finite-sample bounds. The source clarifications state the one-sided score-gap readings. The example and algorithm routes include the printed Durham arithmetic, Mallows insertion probabilities, and pair-location recurrence. Supporting formula presentations remain source context rather than additional named result claims.
The exact Mallows pair-location dynamic program and its PMF semantics are natural candidates for the shared ranking library. No unresolved library certificate supports a final paper conclusion.
docs/DependencyDAG.tex shows the dynamic program as a
green formalized algorithm node downstream of the Mallows
repeated-insertion support. The fixed counterexample remains a separate
green result because its mathematical proof does not rely on trusting
historical plotting code. The rendered
docs/DependencyDAG.pdf is rebuilt from that TeX source and
visually inspected after the update.
The proof endpoints include the displayed rate and finite-sample
clauses. The closeout record
records build and acceptance evidence for its pinned inputs. The
targeted closeout command is
python3 scripts/run_paper_closeout.py --paper GGSG19TopThree --plan-identity <current-plan-identity>.
The checked definitions include common limiting outcome, normalized rate, feasible rate maximization, tier goals, approval mechanisms, Mallows laws, and the repeated-insertion pair-location process and dynamic program.
Propositions 1–4, Theorems 1–2, the Mallows no-randomization corollary, the selected randomization results and counterexample, and the arbitrary-pair dynamic-program correctness and operation bound have checked endpoints.
The current source-to-statement assessment and exact review targets are recorded in the following artifacts. Mathematical scope and qualifications are explained with their named results above.
The 66-item source inventory distinguishes selected result contracts, source models, repeated presentations, and proof support. The selected comparison surface has 15 direct result judgments and 20 prerequisite judgments. Raw empirical data and plots are outside normal theorem scope; the printed Durham arithmetic is retained as a mathematical example.