Updated: 2026-09-05 (current-protocol terminal-document refresh)
The current graph-native surface proves the selected greedy-approximation, truthfulness, payment, and counterexample results.
Formalization gap: twelve selected auction-theoretic
results are proved, while Theorem 6.1’s native NP-hardness and
NP = ZPP consequences remain unproved. Details.
03c97d562cd0e46cc0c93769b55dd8da700173a044653ff7a60653da091e89c5.LOS02CombinatorialAuctions.txt, SHA-256
ac47ef3801288291f7f7e8d0114c31d1a3c79c4649ebeefe660098f63b2625c6.audit/paper_statement_map.json.The selected result surface comprises Theorem 4.1, Proposition 4.2,
Theorem 7.2, the Section-8 and Section-12 negative results, Lemmas
9.1–9.5, Theorem 9.6, and Theorem 10.2. The complete named Theorem 6.1
remains byte-pinned at lines 517–522, but is a partial boundary with
zero proof credit for its NP-hardness and NP = ZPP
conclusions.
The finite bidder and item carriers are explicit. In the selected Sections 7, 9, and 10, legal single-minded requests are nonempty and have nonnegative amounts. The no-ties approximation premise is kept distinct from the fixed, consistent priority used where the source compares tied greedy runs.
| Result | Comparison with source |
|---|---|
| Generalized Vickrey results | Exact: truthfulness and nonnegative truthful utility on the source admissible domain. |
| Square-root greedy bound | Exact: OPT ≤ √m GREEDY for m goods under the source no-equal-norm condition. |
| Example 8.1: greedy allocation with Clarke payments permits profitable misreporting | Exact. |
| Section 12: no payment rule makes greedy allocation truthful for the two-bundle bidder domain | Exact. |
| Section 9 | Exact: critical-value lemmas and truthfulness on the legal single-minded domain. |
| Theorem 10.2 | Exact: average-per-good ordering with Definition 10.1’s first-qualifying-denied-bid payment. |
| Theorem 6.1 | Unproved scope: the source machine-complexity conclusions; see Section 5. |
Theorem 6.1’s native computational-complexity statements are excluded under the explicit public-partial-formalization instruction. No abstract complexity wrapper, reduction helper, or certificate is counted as a proof of that source theorem. This is the sole stated reason the paper remains partially formalized.
None.
None.
None.
The finite auction and critical-price arguments are reusable mathematical support. Native complexity formalization would require a shared machine-level library for reductions, hardness, approximation, and randomized complexity; that future work is outside this paper’s accepted proof surface.
None.
No source correction is asserted. Theorem 6.1’s unproved complexity conclusions are the coverage boundary in Section 5.
PaperInterface.lean exposes one transparent specification for each of the 12 selected source results, and ProofRealization.lean supplies their checked endpoints. The paper-local average-greedy wrapper fixes both the complete average order and the first-denied payment calculation. Theorem 6.1’s machine-complexity conclusion remains the explicit zero-proof boundary described in Section 5.
No standalone Assumptions.lean file is present. Source
conditions appear directly in the expanded specifications. The 18
paper-local prerequisites and five reusable-library prerequisites all
match their source connections in the paper prerequisite ledger and library ledger. Theorem 6.1 is a
coverage boundary rather than an added assumption.
The statement map records the allocation, quasilinear utility, generalized Vickrey, greedy-order, approximation, and critical-payment formulas and model conditions. The source-to-Spec ledger records direct matches for all 12 selected result targets.
The reusable semantic surface consists of the two bundle aliases, quasilinear utility, single-minded bundle size, and allocation value, all reviewed in the library ledger. Generic greedy runners and mechanism containers serve as proof vocabulary rather than separate paper claims.
DependencyDAG.tex was rendered to DependencyDAG.pdf. The graph displays the source model, proof-dependency clusters, and the visible Theorem 6.1 partial boundary without presenting that boundary as a closed result. The rendering was visually inspected for legibility, clipping, and overlap.
The focused-build receipt records a passing proof-interface build. The import-closure receipt and final closure receipt record the checked dependency graph while preserving the paper’s partial status.
The checked definitions and model surface include Definitions 3.1, 3.2, 5.1, 7.1, and 10.1; the allocation and feasibility domains; quasilinear utility; the generalized Vickrey and greedy mechanisms; the square-root objective; the first-denied payment rule; and the Section 8 and Section 12 counterexample models. Exact routes are in the statement map.
The 12 checked result targets cover Theorem 4.1, Proposition 4.2, Theorem 7.2, the Section 8 and Section 12 negative results, Lemmas 9.1–9.5, Theorem 9.6, and Theorem 10.2. The complete Theorem 6.1 machine-complexity statement remains unproved and receives no proof credit.
The source-to-Spec ledger contains 12 current matching judgments, one for each selected proved result. The human review packet is the corresponding reader-facing surface.
The statement map
retains 33 result, definition, model, and condition entries, including
the Theorem 6.1 boundary. No separate
audit/paper_coverage_llm.json is present, so this report
does not claim an additional item-level paper-coverage judgment beyond
the map, the 12 direct result reviews, and the explicit boundary in
Section 5.