Updated: 2026-09-06
The named matching and welfare results are formalized on the domains below.
The source is Monoculture in Matching Markets by Kenny Peng and Nikhil Garg. The formalized scope includes:
Simulations, computational experiments, figures, and narrative conclusion prose are outside the mathematical formalization scope.
| Result | Comparison with source |
|---|---|
| Supply and Demand | Exact. |
| Clearing-cutoff lattice | Exact: market-clearing cutoffs form a complete lattice under the source’s coordinatewise operations. |
| Equal Cutoffs | Additional assumptions: zero score-boundary mass and ranking/noise regularity; necessity for the full claim is unknown. Conditions. |
| Probability formula | Source clarification: atomless noise identifies strict-tail formulas with literal weak matching events. Identity. |
| Proposition 7 | Exact. |
| Proposition 8 | Domain clarified: positive mass is asserted for nonempty open intervals meeting the support interior. |
| Corollary 4 | Current proof conditions: zero score-boundary mass and nondegenerate noise for strict cutoff comparison. Necessity is unknown. Conditions. |
| Theorem 1 | Source clarification: integrable values and atomless value/noise laws; the conclusions use literal weak matching events. Welfare conditions; cutoff regularity. |
| Theorem 2 | Source clarification: atomless noise identifies the literal matching events; eventual advantage also uses atomless values. The positive-mass comparison regions are retained. Conditions. |
| Theorem 3 | Source clarification: atomless values connect market clearing to equality with unrestricted monoculture matching probability. Polyculture probability increases with applications, strictly on the support interior. |
| Differential-access Equal Cutoffs | Current proof conditions: score-level nullity for unique equal cutoffs. Conditions. |
| Finite application game | Restricted scope: ex-ante, same-cardinality deviations; broader deviations remain unproved, and necessity of the restriction is unknown. Game. |
| Lemma 10 | Exact. |
| Uniform maximum example | Typos fixed: mean and Chebyshev denominator. Formulas. |
The application-game scope is stated in Section 6.
None.
The support-interior and strict-tail lemmas should transfer to other continuum cutoff models. The finite application-set comparison may also admit a reusable library abstraction once a second paper needs the same ex-ante success-law semantics.
The Probability Formula and Theorems 1–2 use atomless noise to identify strict tails with weak matching events. Theorem 1 also uses integrable, atomless values; Theorem 2’s eventual-advantage branch and Theorem 3’s market-clearing bridge use atomless values. Necessity of the complete regularity package for the source conclusions is unresolved. Clarification.
The appendix’s unqualified interval and endpoint readings become open-interior statements; singleton intervals and endpoint atoms explain why. The memo gives the exact probability identities and examples.
The qualifications are stated with their results above; necessity of every current-proof condition is not established.
PaperInterface.lean presents each of the 13 selected results once as a transparent target, paired with a checked endpoint in ProofInterface.lean. The literal continuum market, mono- and polyculture laws, rankings, scores, demand, matching, stability, market clearing, cutoff characterization, and analytic theorem chain are implemented in the paper-local files cited by that interface. Supply and Demand and the coordinatewise cutoff lattice cover arbitrary applicant-type probability laws under the cited Azevedo–Leshno market assumptions. Lemma 10 derives cutoff convergence from weak market clearing, including atoms. Theorem 3 derives equality of the baseline and differential monoculture cutoffs from clearing at the same supply, then compares the literal iid choice-event probabilities. With applications its polyculture probability is , including boundary atoms.
Assumptions.lean selects no standalone paper-facing assumption. Source conditions and clarifications appear directly in the expanded targets. The governing Azevedo–Leshno assumptions are separately source-pinned. The current paper prerequisite ledger records the independent review of all 37 routed model and definition declarations.
The statement map routes the market, maximum-order-statistic, cutoff, probability, and differential-access definitions and formulas. The corrected-target distinctions are explained in the source clarification memo and recorded in the source-to-Spec ledger.
The formalization reuses the Azevedo–Leshno cutoff-market layer and general probability infrastructure. PG23-specific value and noise laws, differential-access semantics, and theorem routes remain paper-local. No paper-numbered conclusion is exported as a reusable assumption or certificate.
DependencyDAG.tex presents the source-facing definitions and results in dependency order, including the Appendix observations, Theorems 1–3, differential-access Equal Cutoffs, and the finite no-deviation result. The PDF was compiled and visually inspected on 2026-09-06: the coordinatewise lattice conclusion and Theorem 3 matching probabilities are legible, with separated nodes and visible arrowheads.
The selected source comparisons, complete tracked-paper build, final independent audit, and strict closeout pass. This includes coordinatewise lattice closure, Theorem 3’s choice-event comparisons, and the literal weak-event Theorems 1–2. The closure receipt identifies the accepted evidence.
The checked source definitions are the concrete type-law market, maximum order statistics, and maximum concentration, together with the paper-local cutoff, ranking, matching, stability, market-clearing, and differential-access objects used in the expanded targets. Exact routes appear in the statement map.
The 13 selected results comprise two Appendix support observations, the cutoff-lattice proposition, the three-part threshold lemma, Supply and Demand, Equal Cutoffs, the probability formula, Corollary 4, Theorems 1–3, differential-access Equal Cutoffs, and the finite application-game proposition. The maximum-order-statistic and maximum-concentration definitions remain reviewed model inputs.
The source-to-Spec ledger records 13 result comparisons. The two changed Theorem 1–2 endpoints require successor review. The source clarification memo explains the qualified targets.
The current statement map records 13 selected results and 15 governing prerequisite items routed to 37 Lean declarations. It distinguishes result claims from source definitions and cited model assumptions.