Updated: 2026-09-09
The selected auction revenue and truthfulness results are formalized.
Goldberg, Hartline, and Wright, Competitive Auctions and Digital Goods. The public preliminary paper supplies the theorem numbering and selected auction models and results. Lemma 8.1 and Theorem 8.2 use the later journal version’s monotone-offer condition, explained in the source note. The eight unnumbered Section 11 claims are outside the selected named-theory scope.
| Result | Comparison with source |
|---|---|
| Theorem 4.1; Corollary 4.2; Theorems 7.1–7.2 | Exact asymptotic bounds with domain clarification. The finite logarithmic bounds use largest normalized bid and, for the count bound, at least two bidders. |
| Lemma 6.1 | Exact. |
| Exact-half sampling; bounded dual-price mechanism | Exact with parity clarification. Round half-sizes down for odd inputs; truthfulness and supply feasibility hold for all natural inputs, with exact halves for even inputs. |
| Theorem 6.2 | Exact with count-parameter clarification. The winner-count parameter is a natural number; the stated probability and revenue bounds are proved for uniform half-sampling. |
| Lemma 8.1 | Exact with the journal’s monotonicity condition. Allocation probability increases with the bid under the journal’s cross-bidder offer condition. |
| Theorem 8.2 | Exact with the journal’s monotonicity condition. Expected revenue is at most the optimal fixed-price revenue, including arbitrary real offer distributions. |
| Theorem 9.1 | Exact asymptotic conclusion with source clarification. Integer high-bid examples have and , ruling out a constant competitive ratio for deterministic bid-independent auctions. |
| Lemma 9.2 | Exact. |
| Theorem 9.3 | Exact asymptotic conclusion with source clarification. The same impossibility holds for every truthful deterministic auction in the paper’s set-of-bids model. |
| Bounded-supply rejection | Exact with a selection-rule clarification. If demand exceeds supply, serve accepting bidders in a fixed order independent of their bids. |
None for the selected named-theory results. The eight unnumbered Section 11 claims remain outside that scope.
Lemma 8.1 and Theorem 8.2 use the journal monotonicity condition described in Section 10.
The journal’s inverse-CDF construction is read as the lower generalized inverse, which handles jumps in the offer distribution. The source note explains why this preserves the marginals and revenue argument.
Couple different offer distributions using one uniform random variable to compare their total expected revenue with a fixed-price benchmark.
The formalization additionally proves explicit finite bounds for the asymptotic results.
The memo gives the logarithmic domains, journal monotonicity condition, count and parity conventions, and integer examples for the impossibility results.
The concrete randomized mechanisms use finite distributions; the general auction model allows countable distributions. Theorem 8.2 separately covers arbitrary real offer distributions. The bounded dual-price competitive guarantee is conditional on the stated sampling good-event bounds; the parity convention alone supplies no new odd-input revenue guarantee.
The journal condition narrows the preliminary version’s claim about all truthful auctions; see Section 10. The remaining notes clarify domains and conventions.
PaperInterface.lean states the selected results and ProofInterface.lean supplies their proofs. The selected surface contains 37 model and definition items and 12 result contracts.
The assumption ledger records the eight paper conditions listed in status.json, including the journal monotone-offer condition.
The statement map links revenue, benchmark, sampling, and bounded-supply formulas to their source passages and formal statements.
The real-distribution inverse-CDF argument supplies reusable probability results. Auction benchmarks and source-specific mechanisms remain paper-local.
The dependency diagram, generated from its source, shows how the auction model and benchmarks support the revenue, sampling, and deterministic lower bounds. It was rendered and visually checked on 2026-09-08.
The focused-build receipt, import-closure receipt, and closeout record record validation for their pinned mathematical inputs.
Checked definitions cover auction outcomes, truthfulness, bidder profit, revenue and benchmarks, bid-independent and sampling mechanisms, and unlimited- and bounded-supply models. The statement map records their source connections.
Section 4 lists the selected named results using the preliminary paper’s numbering. The grouped first row covers the logarithmic revenue bounds; Theorem 7.2 includes both the guarantee and its tightness construction.
The source-to-statement review contains six direct matches and six corrected-target matches for the 12 result contracts. The paper-model review contains 73 prerequisite judgments. Their reader-facing interpretation is summarized in Section 4.
The 59-entry statement map contains 49 selected source items, eight unnumbered Section 11 claims outside the selected scope, and two proof-support entries.