is
plain-language theorem explainer
The structure defines the single-item VCG auction under σ-conservation for n agents, with allocation to the highest bidder and winner payment equal to the second-highest bid. Mechanism designers cite it for establishing dominant-strategy incentive compatibility over the full bid space in Recognition Science auctions. The declaration is a direct structure with zero proof lines, extending from upstream collision-free and phase-lift results.
Claim. For $n$ agents with bids $b_i$, the mechanism allocates the item to $i^* = $ argmax $b_i$ and sets the winner's payment to $m = $ max$_{j ≠ i^*} b_j$, with all losers paying zero.
background
The module sets VCG as the σ-conserving auction in track E10, replacing prior stubs that only handled the trivial case others_value = 0. It uses the allocation rule to the highest bidder and the Clarke pivot payment rule. Upstream results supply the collision-free class from OptionAEmpiricalProgram.is, the algebraic tautology of EdgeLengthFromPsi.is, the verified structure of MockThetaPhantom.is, the log-derivative bound of CirclePhaseLift.and, and the cyclic successor of EightTick.next.
proof idea
Zero-line structure definition with no tactics or lemmas applied; the components are declared directly from the combinatorial setup.
why it matters
Supplies the core mechanism feeding downstream results including optimalT60, hearingLossPenalty, energyConservationCert, and christoffel. It completes the E10 track by encoding DSIC for σ-conserving auctions and connects to the eight-tick octave via EightTick.next. The open extension to general n appears in the next file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.