Updated: 2026-09-09
The paper’s threshold-sufficiency results are formalized: after screening, threshold allocation policies achieve the required utility, cost, and fairness constraints.
Cai, Gaebler, Garg, and Goel, Fair Allocation through Selective Information Acquisition, AIES 2020 / arXiv v3. The scope covers Theorem 2, Appendix Lemmas 4–5 and 7, Appendix Theorem 6, and their model and threshold-policy definitions. The standalone linear programs, empirical simulations, and runtime discussion are outside this scope.
| Result | Comparison with the paper |
|---|---|
| Definition 1; Appendix Definition 3 | Exact. |
| Theorem 2; Appendix Theorem 6 and Lemma 7 | Exact with source clarification. Expected utilities condition on the full vector of observed estimates used for allocation, and the equal-cost comparison covers every permitted threshold. |
| Appendix Lemma 4 | Exact with source clarification. Reading. |
| Appendix Lemma 5 | Exact after correcting a typo. Interpolation; posterior reading. |
None.
None.
Appendix Theorem 6 needs the equal-cost comparison for every possible threshold. The proof extends that comparison to nonpositive cutoffs and both infinite endpoints; see the threshold proof note.
None.
None.
The posterior reading conditions utility estimates on all information observed by the allocation rule. Appendix Lemma 5 has a typo in its interpolation probability; correcting it preserves the stated utility and cost conclusions.
None.
PaperInterface.lean states the selected results; ProofInterface.lean connects them to their proofs.
The positive-cost and exogenous-screening readings, and the full-vector posterior reading used by full-vector allocation, are source clarifications. They make the information and policy interpretation used by the displayed model explicit; none is an additional economic assumption.
The linear-program displays support the allocation model. They are not additional named theorems in the selected scope.
The proof reuses Mathlib’s representation of a policy that depends only on observed information.
The dependency diagram connects the screening and allocation model to the threshold definitions, Appendix results, and Theorem 2.
The paper build and independent mathematical review passed. The closeout record links the retained evidence.
Paper statement. A solution to the constrained problem can be replaced by a threshold allocation after the screening policy is fixed.
Status. formalized.
Paper statement. A positive cost-aware threshold policy is not dominated at equal cost or equal utility.
Status. formalized.
Paper statement. Achievable expected utility or expected cost targets can be attained by cost-aware threshold policies.
Status. formalized; the source interpolation display is clarified in Section 10.
Paper statement. Cost-aware threshold policies suffice, including when the diversity inequalities are replaced by equality constraints.
Status. formalized.
The statement review compares the selected results with the paper; the model review checks their governing definitions and assumptions.
The source inventory covers the five named results and their three governing model or definition records. The standalone linear-program displays remain supporting material.