Updated: 2026-09-05
The four main attenuation and amplification theorems are proved with their published conclusions.
Formalization gap: Proposition 1 and Propositions 7(ii)–8 have their qualitative limits proved, while the source polynomial rates remain unproved. Details.
The source is Wisdom and Foolishness of Noisy Matching Markets by Kenny Peng and Nikhil Garg. The formalized scope includes the basic and extended coalition economies; Hölder value-law and capacity regularity; beta-max-concentrating and long-tailed noise; cutoff stability and match probability; Theorems 1–4; and the named results in the attenuation and amplification appendices. Simulations, figures, examples, and narrative interpretation are outside the mathematical source inventory.
The two source-model bundles were checked as prerequisites and do not contain the theorem conclusions they support.
| Result | Comparison with the paper |
|---|---|
| Theorems 1–4 | Exact. |
| Proposition 1 | Tail typo fixed; polynomial-rate proof gap: matched
mass below the threshold replaces the impossible printed upper-tail
display. Uniform qualitative vanishing is proved; the intended
O(C^{-K(β,γ)}) rate remains unproved. |
| Propositions 2–5 and Lemma 6 | Exact. |
| Proposition 7(i) | Exact. |
| Proposition 7(ii) and Proposition 8 | Proof gaps: qualitative convergence is proved, while both printed polynomial rates remain unproved. No counterexample refutes either rate under the full source assumptions. |
| Propositions 9–10; Lemmas 11–13; Propositions 14–15 | Exact. |
| Coalition conditional laws | Statement clarified: conditional kernels are specified almost everywhere on the value-law support. |
For source locations and concise mathematical explanations, see the source clarifications.
None in the checked endpoints. A suitable one-draw lower-tail bound would support the printed Proposition 7(ii) route and its downstream polynomial rates, but the current formalization neither assumes such a bound nor derives it from maximum concentration.
The attenuation proof uses a source-faithful finite dense-cluster/large-gap construction with natural-number rounding, a genuine cutoff partition, exact capacity accounting, and atom-safe event bounds. The amplification proof uses an interior support anchor and finite long-tail shifts to transport the quantile-window estimate to an arbitrary real target. The exact local replacements and their reasons are in the appendix memo.
The proofs consume existing reusable probability, finite-product, order-statistic, and cutoff-market infrastructure. Paper-specific cutoff geometry, coalition witnesses, and source corrections remain paper-local. The direct review checks reusable declarations by exact Lean body and source connection; it does not treat a declaration name or an imported theorem as semantic evidence.
No additional generalization is claimed.
The source memo supplies the exact tail/rate qualifications in Section 5 and proof replacements in Section 7.
The polynomial rates in Proposition 1, Proposition 7(ii), and Proposition 8 remain unproved. The qualitative replacements suffice for Theorems 1–4. The missing one-draw estimate has not been derived from maximum concentration, and no counterexample here refutes the full source rate claims.
PaperInterface.lean exposes the two source models, the four main theorems, and the selected attenuation/amplification appendix claims as transparent targets. ProofInterface.lean contains their checked endpoints, including the lower-tail and qualitative-rate repairs identified in Sections 4–5.
No additional assumption beyond the source models is used. Four primitive model rows have current matching judgments in the paper-prerequisite ledger. Coalition conditional laws use the almost-everywhere support reading stated in Section 4.
The source map binds beta-max concentration, long-tail noise, cutoff stability, match probabilities, capacity rounding, tail events, and appendix rate displays. The source memo records the corrected tail orientation, qualitative replacements, and local proof-formula fixes.
The proofs use reusable probability, finite-product, order-statistic, and cutoff-market infrastructure. Paper-specific cutoff geometry, coalition witnesses, and source corrections remain paper-local; no separate material library review row is selected by the current graph.
The dependency DAG groups the literal models, four main theorems, and fifteen appendix endpoints by proof role. Its retained 2026-09-05 visual inspection found readable labels and arrow directions, with no clipping, node overlap, or edge crossing through node interiors.
The accepted graph records twenty-five matching direct source-to-Spec judgments and four matching model prerequisites. The coverage ledger separates ten direct covered items from fifteen support-only appendix items. Retained focused paper builds and the independent source review passed. See the accepted graph and closure receipt.
Checked definitions include the holder/value and capacity models, beta-max-concentrating and long-tailed noise, stable-matching cutoffs, match probability, attenuation/amplification events, coalition value laws, and the finite rounding and support constructions used in the appendices.
The direct comparisons are in the source-to-Spec ledger; model rows are in the paper-prerequisite ledger, and correction provenance is in source-proof fidelity.
The coverage ledger records ten direct covered items and fifteen support-only items. The source map also retains the primitive models and correction records. The four main theorems keep their source conclusions; the appendix rate qualifications remain visible in Sections 4–5 rather than being counted as exact printed rates.