Updated: 2026-09-09
The selected approximation, truthfulness, payment, and counterexample results are formalized. Theorem 6.1’s computational-hardness conclusions remain unproved.
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. |
| Square-root greedy bound | Exact. |
| 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. |
| Theorem 10.2 | Exact. |
| Theorem 6.1 | Formalization gap. The finite reduction is proved, but NP-hardness of optimal allocation and the claim that beating the square-root approximation barrier in polynomial time implies remain unproved. |
Theorem 6.1’s native NP-hardness, approximation-hardness, and
NP = ZPP conclusions remain unproved. The checked finite
reduction maps a clique instance through graph complementation and
unit-weight set packing to the auction decision problem. It includes an
injective varying-size binary encoding, semantic correctness, and
polynomial bounds for the explicit incidence-table map.
These results establish the reduction’s finite construction and its stated operation counts. They do not supply a native machine-model hardness theorem or the randomized complexity-class consequence. The source hardness construction uses unit bids, which the encoding covers; encoding arbitrary real-valued optimization inputs is a separate remaining boundary.
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.