Updated: 2026-09-04
The paper’s selected named theoretical surface is formalized: the two printed college-admissions definitions, the Section 3 marriage-instability definition, and Theorems 1–2. The Section 4 conclusion that the waiting-list procedure terminates in a stable assignment is also checked as the source result needed to read Theorem 2. Independent reviewer annotations may be added through the packet or dashboard, but are not a prerequisite for this formalization status.
| Result | Comparison with source |
|---|---|
| Theorem 1 | Exact: finite stable-marriage existence for strict complete preferences by deferred acceptance. |
| Theorem 2 | Stability notion clarified: applicant optimality uses the full operational stability of Sections 4–5. Reading. |
| Section 4 | Exact: the simultaneous waiting-list procedure terminates with a stable assignment. |
| Printed definitions | Exact: the page-10 replacement-pair and optimality definitions, within their fixed-quota domain, and the separate marriage-instability definition. |
None within the selected named theoretical surface.
None.
None.
The source supplies two complementary reusable finite procedures. For Theorem 1, deferred acceptance maintains tentative partners while rejected applicants continue proposing, and termination yields stability. For Theorem 2, define a college to be possible for an applicant when some stable assignment sends the applicant there, then use induction over the rejection steps to show that the procedure never rejects an applicant from a possible college. This turns the algorithmic trace into the applicant-optimality comparison.
This closeout makes no claim beyond the paper’s stated marriage and college-admissions results. In particular, it does not treat the paper’s unnumbered extensions or numerical examples as separately formalized theorems.
Theorem 2 uses the full operational stability of Sections 4–5, including vacancy blocks and mutual acceptability. Page 10’s replacement-pair definition remains a separate literal claim. The memo explains the distinction.
None within the reviewed named theoretical surface. The distinct scope of the page-10 definition and the completed Sections 4–5 reading is a clarification, not a caveat on either theorem.
The checked surface comprises the page-10 definitions of unstable and optimal college assignments, the Section 3 definition of an unstable marriage, Theorem 1, the Section 4 terminal-stability conclusion used by Theorem 2, and Theorem 2. PaperInterface.lean presents the six selected claims, and ProofInterface.lean supplies the checked proof endpoints.
The statement map anchors the college definitions to the fixed-quota model and the marriage and waiting-list results to their source sections. The two retained paper-local prerequisites match their source connections in the prerequisite ledger. No standalone paper-facing assumption declaration is selected.
No displayed algebraic formula is selected as a separate result. The two page-10 definitions and the Section 3 instability definition are preserved as their own source-facing targets, with exact locations and Lean routes in the statement map.
The library semantic ledger selects no material reusable-library prerequisite. The deferred-acceptance and waiting-list models used for these results remain paper-local.
DependencyDAG.tex was compiled to DependencyDAG.pdf. The rendered PDF was visually inspected for readable labels, logical reading order, arrowheads, and node or edge overlap.
The focused-build receipt records a passing paper build. The source-to-Spec ledger records six matching judgments, while the import-closure receipt and final closure receipt record the checked Lean closure and terminal graph.
The checked definitions are unstable college assignment, optimal stable college assignment in the fixed-quota domain, and unstable marriage. The waiting-list procedure model is retained as the source context for the terminal-stability result and Theorem 2.
The source-to-Spec ledger contains six direct matches. The human review packet presents the same definitions and claims in dependency order.
The coverage ledger contains five covered named-theory items: the three definitions and Theorems 1–2. The Section 4 terminal-stability conclusion is retained as a separate direct proof route for Theorem 2 in the source-to-Spec ledger. The full model and route inventory is in the statement map.