Final Validation Report: Strategic Ranking

Updated: 2026-09-09

1. Human Verdict

The equilibrium, welfare, utility, and fairness results are formalized. Proposition 3.1’s cutoff-monotonicity claim and Proposition B.2’s weighted optimum require the additional conditions stated below.

2. Closeout Status

• Completion status: formalized
• One-sentence recap: All 18 selected results are proved, with local restrictions for two optimization claims.

3. Source and Scope

Liu, Garg, and Borgs, Strategic Ranking, AISTATS 2022, PMLR 151, pp. 2489–2518. The scope includes the 18 named results in the main text and supplement, with their governing definitions. Empirical implementation and unnumbered social-welfare discussion are outside this scope. The model note explains tie priorities and continuum equilibrium.

4. Researcher Summary of Checked Results

The source clarification note states the conditions, formulas, counterexamples, and proof changes in mathematical terms.

5. Remaining Boundaries and Gaps

All 18 selected results are proved on the stated domains. The unrestricted versions of Proposition 3.1’s cutoff monotonicity and Proposition B.2’s weighted optimum are false; the additional conditions are in Section 6.

6. Additional Assumptions Beyond Paper

For Proposition 3.1’s monotonicity clause only, put $E=p^{-1}(1)$ and $C=p\circ g^{-1}$. Require concavity of $x\mapsto\log f(1-e^{-x})$ on $x>0$, and of $z\mapsto\log C(e^z)$ where $g(0)<e^z\le g(E)$. No zero-baseline-production or positive-minimum-skill restriction is added. The unconditional pure-randomization optimum does not use these premises.

For B.2 only, measurable skill is affine and nondegenerate with nonnegative lower endpoint. Require $g(0)=0$, $B\ge E=p^{-1}(1)$, concavity of $g^2$ on $(0,B)$, convexity of $x/C(x)$ on $[g(p^{-1}(\rho)),g(E)]$, twice differentiability of cost and production on their stated open domains, and continuity of $g''$. Keep source endpoint continuity and independent regular unmeasurable skill. The full B.2 statement spells out conditional means and the policy domain. No supporting-line or optimizer property is assumed.

Known priorities, the strong applicant-wise AE quantifier, the hard residual budget in B.2, and weak/strict interpretation are model/statement clarifications. They are not additional economic shape assumptions.

7. Proof-Strategy Deviations

The proof uses the correct welfare derivative, normalized utilities and admissible witnesses, and the source effort-comparison indices. For Proposition B.2, utility curvature establishes a global optimum; a zero derivative alone would not suffice.

8. Proof Tricks Worth Reusing

Useful techniques include preserving rewards within rank bands, comparing equilibria under changes on null sets, integrating normalized tail means, and deriving globally optimal weights from utility curvature.

9. Generalizations, Conjectures, and Extensions

The welfare skill condition is strictly broader than log concavity. For differentiable interior skill it is equivalent to $(1-t)f'(t)/f(t)$ being nonincreasing. The quantile $1/(2-t)$ separates the conditions. Every technology $p(e)=e^r,\ g(e)=e^s$, $r>1,\ 0<s\le1$, satisfies the score-cost condition, including uniform skill on any nondegenerate nonnegative interval. These are proved supporting extensions, not extra source claims. The conditions are sufficient, not claimed necessary. Mathematical statement.

10. Source Clarifications and Exact Readings

The memo explains the local formula and proof clarifications. The weak and strict welfare comparisons need no additional economic assumption; derivative claims apply where the derivative exists. The two substantive restrictions are stated in Section 6.

11. Paper Issues or Caveats

Proposition 3.1’s unrestricted cutoff-monotonicity claim and Proposition B.2’s every-cutoff optimum have counterexamples. Their restricted versions are proved under the conditions in Section 6.

12. Detailed Formalization Evidence

PaperInterface.lean states each selected result; ProofInterface.lean supplies its proof. The comparison uses actual equilibrium score distributions and all feasible deviations.

13. Paper Assumption Provenance

The source cost, production, skill, policy, and equilibrium assumptions are recorded in the model review. The two additional sets of conditions are stated in Section 6.

14. Displayed Formula Provenance

The source map links each named result and its formulas to the formal statement. The memo distinguishes the restricted claims from their unrestricted printed versions.

15. Library Lift Pass

The proof reuses the shared probability, measure, order, and convexity layers. General tie-rank and probability-integral-transform work is available in the shared foundation. Paper-specific population, incentive, and utility bridges remain in the paper modules. The upper-tail skill and power-technology extensions are proved locally; no external unpinned Lean code is imported.

16. DAG Audit

The paper-facing DAG displays all 18 named results and their governing mathematical dependencies. The two local restriction nodes are distinct from ordinary clarified results, and B.1 has no fixed budget. The diagram compiled and was visually inspected: labels, arrowheads, reading order, and node boundaries are legible without overlap. The diagram source is retained. The independent terminal audit also passed.

17. Validation Checks

The paper build, independent mathematical review, final audit, and strict closeout passed on September 9, 2026. The closeout record links the evidence. Human result annotations remain 0/18.

18. Paper Definitions Checked

The source inventory covers the scalar cost/production/skill model, finite and two-level policies, actual tie-broken ranks, individual best response and equilibrium, pure randomization and deterministic admission, applicant/private/societal utility, group population and mixture ranks, clipped group thresholds, welfare gaps and access, exchangeable multidimensional costs, the hard-budget multitask model, and conditional weighted utility. These are semantic declaration routes, not reflexive proof wrappers.

19. Named Theorem Statements Checked

Section 4 lists the ten main-text and eight appendix results. Their proofs cover the domains and conditions stated there.

20. Statement and Validation Records

The statement review and model review record the comparison with the source. The closeout record selects the accepted evidence.

21. Source-Coverage Audit Ledger

The source inventory includes all 18 named results and their governing definitions. The unnumbered social-welfare footnote remains supporting discussion, outside the selected theorem scope.