Updated: 2026-09-07
The paper’s named theoretical results are proved on the domains stated below. Shared clarified regularity conditions are consolidated once in Section 6; genuine source corrections remain result-local.
The source is arXiv:2307.15142. The scope includes Equation (4), Definitions 1–3, the named main-text results, and Appendix Lemmas D.1–D.5. Example 1 remains supplemental illustrative material; its continuous relaxation does not receive whole-example credit. Simulations, figures, captions, and other numerical observations are outside this scope.
| Result | Comparison with the paper |
|---|---|
| Example 1, continuous top-one relaxation (Equation 2) | Supplemental illustration. The continuous relaxation is proved; Example 1 as a whole is outside the selected result scope. |
| Equation (4); Definitions 1–3; Proposition 5; Lemma 1 | Exact. |
| Corollary 1 | Exact with clarified regularity conditions. |
| Theorem 1(i) | Corrected target: the finite-discrete conclusion needs a nondegenerate top-value split; a point-mass law does not force uniform optimal shares. |
| Theorem 1(ii)–(iv) | Exact with clarified regularity conditions. |
| Theorem 1(v) | Additional sign condition: the common conditional mean is nonnegative. A negative mean reverses the maximal-weight choice; at zero mean every allocation ties. |
| Proposition 2 | Source correction: a compiled strictly-positive-PMF
counterexample refutes the printed (T+1)/N constant. The
checked (2T+1)/N bound retains the same square-root
limit. |
| Theorem 2 | Source clarification: independent Bernoulli coordinates with rank-dependent probabilities. |
| Appendix Lemma D.1 | Changed statement: corrected sign regimes and deficit comparison replace the printed asymptotic branches. |
| Appendix Lemmas D.2–D.5 | Restricted scope: eventual valid ranks and the corrected strictly-concave rounding statement. |
| Proposition 4, Equations (18) and (20) | Formulas corrected: Equation (18) is an inequality; Equation (20) uses the preference-weighted measure from Equation (17). |
| Proposition 4, limit step | Exact with clarified regularity conditions. |
| Theorem 3; Corollary 3 | Restricted scope: nondegenerate Bernoulli endpoint domains. |
The corrected Proposition 2 finite constant and the other result-local source corrections are stated in Sections 4 and 7. Shared model domains are in Section 6, and the Theorem 2 reading is in Section 10. Computational claims are outside this theoretical scope.
These clarified regularity conditions state the common domains for the rows marked Exact with clarified regularity conditions. They do not convert a false source claim, a changed finite constant, or a non-equivalent repair into an exact reading.
k value model, conditional values are
nonnegative almost surely. This makes the source top-k
value primitive coincide with the finite allocation objective used for
Theorem 1(i)–(ii); Theorem 1(i)’s separate nondegeneracy repair remains
visible in its own row.(0,1]. The density need not be continuous: it aligns
preference and volume null sets, while radial continuity rules out a
pointwise Laplace maximum supported only on a null spike.Theorem 1(v)’s sign condition and the Bernoulli endpoint exclusions are separate result-local restrictions. See the source clarification record.
The checked Proposition 2 allocation is and gives the finite bound . A compiled strictly-positive-PMF witness refutes the paper’s bound under its printed finite model. The asymptotic square-root shares are unchanged. Exact comparison.
The memo also gives D.1’s deficit and maximization comparisons and Proposition 4’s measure correction.
A positive probability-mass atom gives a direct positivity proof for the finite normalizer in the gamma-share argument.
A supportwise treatment of zero-PMF coordinates could generalize the all-coordinate share results, but it is not represented as an already-proved extension. Any such extension should first specify whether coordinates with zero selection probability are excluded or assigned a separate convention.
Theorem 2’s rank-dependent Bernoulli probabilities are independent but cannot also be identically distributed. The clarified regularity conditions apply only to the rows identified in Section 6; the order-statistic and rounding domains and other result-local corrections remain separately stated.
The formalization boundaries are stated in the limited-scope paragraph and Sections 4–6. Proposition 2’s sharper printed finite bound is false under its printed model; its checked counterexample and corrected constant are visible in Sections 4 and 7.
The selected surface contains 25 transparent result specifications from PaperInterface.lean, and ProofInterface.lean supplies their checked endpoints. The surface covers Equation (4), Definitions 1–3, the named main-text results, and Appendix Lemmas D.1–D.5 within the domains and corrected statements summarized in Section 4.
The seven reviewed paper prerequisites expose the model definitions and source conditions used by the selected results. Their result-specific positivity, support, endpoint, and regularity conditions are stated in Sections 4, 6, and 10 and the source clarification memo.
The statement map routes 18 formula presentations and three equation presentations, including Equation (4), the homogeneity and order-statistic formulas, the Proposition 2 allocation and bound, and Appendix D asymptotics. The source-to-Spec ledger records the exact or corrected-target status of each selected result.
The library semantic ledger selects no material reusable-library prerequisite. The accuracy-diversity model, allocation, order-statistic, and asymptotic constructions remain paper-local.
The one-page DependencyDAG.pdf, generated from DependencyDAG.tex, was visually inspected at 180 dpi on 2026-09-07. Its metadata, legend, node labels, borders, and arrows are legible, with no observed clipping or label/box overlap.
The import-closure receipt records the paper import surface. The closeout record records build and acceptance evidence for its pinned inputs. The review packet presents the current selected statements and governing definitions.
The targeted terminal command is
python3 scripts/run_paper_closeout.py --paper PRPKG24AccuracyDiversity.
The checked definitions are Equation (4)’s representation, Definition 1’s gamma homogeneity, Definition 2’s sequence homogeneity, and Definition 3’s order-statistic mean. The source map also retains the model and formula conditions used by their dependent results.
The 25 selected result targets cover Theorems 1–3, Corollaries 1 and 3, Propositions 2, 4, and 5, Lemma 1, and Appendix Lemmas D.1–D.5, with separate clauses for multipart results. Equation (4) and Definitions 1–3 are reviewed as governing definitions. Section 4 gives the source comparison.
The source-to-Spec ledger contains 25 selected judgments: eight matches and 17 corrected-target matches. The corrected statements and restrictions are explained in the source clarification memo.
The statement map retains 70 source items, including model definitions, formulas, examples, and named results. The current selected comparison consists of 25 result judgments and seven paper-prerequisite judgments; source context is not counted as a separate proved result.