Updated: 2026-09-06
The named auction bounds are proved on the stated parameter and randomization domains. The journal monotone-offer condition supplies the source reading for Lemma 8.1 and Theorem 8.2.
Formalization gap: Lemma 8.1 and Theorem 8.2 are proved for finite offer support; continuous-offer cases remain unproved. Details.
formalized.The public SODA paper PDF is the primary source version for the normal inventory. Normal scope contains 49 source-presented items: 37 definitions and 12 named results. Forty-three retain their source endpoints. Four make their nondegenerate domains explicit, while the later journal text supplies the Lemma 8.1 and Theorem 8.2 corrections. Eight unnumbered Section 11 prose claims are outside this named-theory surface.
| Result | Comparison with source |
|---|---|
| Theorem 4.1; Corollary 4.2; Theorems 7.1–7.2 | Restricted domains: largest normalized bid at least two, or at least two bidders. The logarithm is undefined at one; necessity of excluding bids strictly between one and two is unknown. Domains. |
| Lemma 6.1 | Exact. |
| Exact-half sampling; bounded dual-price mechanism | Restricted mechanism: equal-half partitions and even total supply; other cases remain outside the proved mechanism. Necessity of these restrictions is unknown. Scope. |
| Theorem 6.2 | Restricted scope: a natural-number count parameter; extension to real parameters requires an unproved rounding step. This is a current proof restriction. Scope. |
| Lemma 8.1 | Source-version correction; formalization gap: journal monotone offers, but finite offer support only. Continuous offers remain unproved; finite support is not shown necessary. Condition and scope. |
| Theorem 8.2 | Source-version correction; formalization gap: journal monotone offers, but finite offer support only. Continuous offers remain unproved; finite support is not shown necessary. Condition and scope. |
| General randomized auctions | Restricted scope: countably supported outcome laws. Continuous-law extensions remain unproved; necessity of countable support is unknown. Scope. |
| Theorem 9.1 | Restricted construction: the bid-independent lower bound uses integer high bids. Construction. |
| Lemma 9.2 | Exact: deterministic truthfulness implies bid independence under the source participation/payment conditions. |
| Theorem 9.3 | Restricted construction: integer high bids in the deterministic erased-multiset model. Construction. |
| Bounded-supply rejection | Specified selector: fixed report-independent priority among accepted bids. Scope. |
The continuous-offer cases of the randomized-auction results remain unproved. The checked logarithmic and count-parameter ranges are stated in Section 4; their proof restrictions are not established as necessary for all source conclusions.
The general randomized-auction model is formalized for countably supported outcome laws, and Lemma 8.1/Theorem 8.2 for finite offer support. The logarithmic bounds use the explicit domains in Section 10. These are conditions of the checked statements, not claims that the broader source results require these exact restrictions. The bid multiset and bounded-supply priority conventions instantiate the source auction model.
The source clarification memo gives the formulas, journal monotone-offer condition, and effect of each scope choice.
None.
None.
No additional generalization is claimed by this closeout.
Section 5 records the randomization and parameter coverage gaps. The journal monotone-offer correction is separate from those formalization limits.
The selected source surface comprises 37 source semantic declarations and 12 result contracts. PaperInterface.lean exposes the result targets, and ProofInterface.lean supplies their separate proof endpoints. The current saved Lean graph retains the actual definitions and mechanisms; 73 paper-local prerequisites have current semantic judgments. The selected surface covers the unlimited- and bounded-supply auction models, sampling mechanisms, weighted pairing, truthfulness, revenue bounds, and lower bounds described in Sections 3–4.
The eight declarations listed in status.json are all judged paper conditions in the assumption ledger. Their result-level scope, including the journal monotone-offer condition and finite-support restrictions, is stated in Sections 4, 6, and 10 and in the source clarification memo.
The statement map records the auction, revenue, benchmark, sampling, and bounded-supply formulas with their source routes. The source-to-Spec ledger contains six direct matches and six corrected-target matches for the 12 result contracts. The 73 paper-local prerequisite judgments cover the actual governing definitions and mechanisms. The result-specific domains and journal corrections remain those summarized above.
The library semantic ledger selects no material reusable-library prerequisite for separate review. The finite-auction objects and the source-specific benchmark and mechanism constructions remain paper-local.
DependencyDAG.pdf, generated from DependencyDAG.tex, was visually inspected on 2026-09-03. The single-page graph has legible labels and no clipping or overlap; its arrows show the core-model/benchmark, sampling/Lemma 6.1/Theorem 6.2, weighted-pairing/Theorem 7, and deterministic/bounded-supply routes.
The current planner reports reusable compiled inputs, current semantic review, and current graph-native proof realizations. The import-closure receipt records the Lean import surface. The focused-build receipt and final closure receipt record the most recently completed checks; the successor strict transaction verifies its own focused build and final inputs before issuing a current closure credential.
The checked definitions include revenue and truthfulness; single-price, fixed-price, weighted-pairing, and bounded-supply benchmarks; auction outcomes, mechanisms, bidder profit, price classes, threshold and bid-independent auctions; the unlimited- and bounded-supply models; and the source’s sampling mechanisms. Exact routes appear in the statement map.
The selected result surface contains the Theorem 4.1 and Corollary 4.2 bounds, Lemma 6.1 and Theorem 6.2 sampling results, the Theorem 7 weighted-pairing bounds, the corrected Lemma 8.1 and Theorem 8.2 statements, and the Section 9 bid-independent and deterministic lower bounds, together with the bounded-supply extensions summarized in Section 4. Exact target/endpoint pairings are in PaperInterface.lean and ProofInterface.lean.
The source-to-Spec ledger contains 12 current result judgments: six matches and six corrected-target matches. The paper-prerequisite ledger records 73 matches; no separate library prerequisite is selected. The distinctions behind the corrected targets are stated in the source clarification memo.
The 59-entry statement map contains 49 selected source items: 37 source semantic declarations and 12 result contracts. Eight Section 11 assertions remain deep-audit material, and two rows are proof support. The current direct and prerequisite ledgers supply the selected semantic evidence; the older coverage ledger retains the earlier 49-item presentation and is not a new result denominator.