Updated: 2026-09-09
The paper’s noise-attenuation and noise-amplification results are formalized. The appendix’s one-draw tail estimates use a finite second moment, as detailed below.
The source is Wisdom and Foolishness of Noisy Matching Markets by Kenny Peng and Nikhil Garg. The checked source surface includes the basic and extended-coalition economies; value-law and capacity regularity; beta-max-concentrating and long-tailed noise; cutoff stability and match probability; Theorems 1–4; and the named appendix propositions and lemmas supporting them. Simulations, figures, examples, and narrative interpretation are outside this mathematical scope.
| Result | Comparison with the paper |
|---|---|
| Theorems 1–4 with the appendix proof corrections | Exact. |
| Appendix Proposition 1, with its one-draw rate condition | Exact after correcting the tail typo, under an additional regularity condition. The polynomial lower-tail rate uses a finite second moment for one noise draw. |
| Appendix Propositions 2 and 5; Appendix Lemma 6 | Exact after correcting typos. The intermediate algebra and probability calculations are corrected. |
| Appendix Proposition 3 | Exact after correcting the block-endpoint typo. The high-cutoff block includes the pivot. |
| Appendix Proposition 4 | Exact after correcting the block-endpoint typo. The high-cutoff block includes the pivot. |
| Appendix Proposition 7(i) | Exact. |
| Appendix Proposition 7(ii) | Exact under an additional regularity condition. The near-one rate uses a finite second moment for one noise draw. |
| Appendix Proposition 8 | Exact under an additional regularity condition. The lower-tail integral rate uses the same finite-second-moment condition. |
| Appendix Proposition 9; Appendix Lemmas 11–13 | Exact. |
| Appendix Propositions 10, 14, and 15 | Exact with source clarification. |
| Coalition conditional laws | Exact. |
No proof gap remains in the selected scope. The additional condition for three appendix results is stated in Section 6.
Appendix Proposition 1, Appendix Proposition 7(ii), and Appendix Proposition 8 use the explicit finite-second-moment condition for one iid noise draw. It supplies the one-draw Chebyshev calculation; beta-max concentration by itself controls maxima rather than this single-draw quantity. The source clarifications give the result-level scope. No additional condition is used for the four main theorem statements.
The appendix proofs use corrected capacity algebra, event inclusions, natural-number rounding, atom-safe tails, and a finite long-tail-shift bridge for the all-real amplification conclusion. These repairs preserve the displayed conclusions; their result-level descriptions are in the source clarifications.
The development uses reusable probability, finite-product, order-statistic, and cutoff-market infrastructure. It adds a reusable one-sided Chebyshev lower-tail bound for a real probability law with finite second moment; market-specific cutoff geometry and source corrections remain paper-local.
None.
The source clarifications give the source anchors, corrected formulas, and result-level effects for every material correction or added condition in this report.
The three appendix rates above are formalized under the stated one-draw finite-second-moment condition. The source corrections do not alter the economic primitives or the main theorem conclusions.
PaperInterface.lean states the paper-facing results and ProofInterface.lean proves their endpoints. The human review packet presents the source statements, formalized targets, and proof endpoints together.
The basic and coalition market models, regularity conditions, noise conditions, cutoff characterization, and match-probability formula are checked directly against the source. The finite one-draw moment used by the three corrected appendix rates is described in Section 6.
The source map records each selected result’s source anchor and transparent paper-facing target. The source clarifications identify every material corrected formula.
The reusable lower-tail Chebyshev inequality supports the paper’s one-draw rate argument. Other probability and matching tools are ordinary reusable foundations; no external Lean formalization was imported.
DependencyDAG.tex and DependencyDAG.pdf organize the source models, named appendix results, and four main theorems without implementation-helper nodes. The rendered DAG was visually inspected for labels, arrowheads, reading order, and node or edge overlap.
The closeout checks the complete paper-owned Lean module surface, each transparent source-to-Spec target, its proof endpoint, its prerequisite surface, and the absence of untrusted proof boundaries. The closure receipt records the final accepted graph.
The targeted closeout command is
python3 scripts/run_paper_closeout.py --paper PG24NoisyMatchingMarkets
with the planner-issued identity.
Checked definitions include the two market models, regularity and noise conditions, stable cutoffs, match probability, attenuation and amplification events, coalition value laws, and the finite rounding constructions used in the appendices.
The source-to-Spec ledger records the independent direct reviews; the paper-prerequisite ledger records the paper-model reviews; and source-proof fidelity records the source corrections.
The source map retains the selected named result inventory, byte-pinned source anchors, and their transparent formalized targets.