was
plain-language theorem explainer
Game theorists in the Recognition Science program cite this scaffolding result to ground dominant-strategy incentive compatibility for the single-item VCG auction inside sigma-conservation. The declaration encodes the allocation to the highest bidder and the payment rule that charges the winner exactly the runner-up bid. The current proof is a sorry stub that must be replaced by case analysis on whether a deviation changes the winner or the payment amount.
Claim. For $ngeq 2$ agents indexed by $mathrm{Fin},n$, each with private valuation $v_iinmathbb{R}_{geq0}$ and submitted bid $b_iinmathbb{R}$, the mechanism allocates the item to the highest bidder $i^*$ (ties broken by lowest index) and charges that winner the second-highest bid while charging all others zero. The mechanism satisfies dominant-strategy incentive compatibility: for every agent $i$ and every fixed vector of others' bids, the utility obtained by reporting $b_i=v_i$ is at least as large as the utility obtained by any other report $b_i'$.
background
The module replaces an earlier placeholder whose only content was the trivial identity on summed agent values. It defines a concrete single-item auction whose allocation rule selects the argmax bidder and whose payment rule is the Clarke pivot: the winner pays the highest competing bid. Utility for an agent is then valuation minus payment when winning and zero when losing. This construction makes the total surplus under truthful reports equal the winner's valuation, which is the local form of sigma-conservation on the utility ledger.
proof idea
The proof is a sorry stub. A completed version would fix the other agents' bids, unfold the definitions of winner, payment and utility, then perform case analysis on whether the agent's reported bid equals the true valuation or changes the allocation outcome, verifying the resulting inequality in each branch by direct comparison of the two possible payments.
why it matters
The declaration supplies the mechanism-design primitive that downstream results such as main_resolution in ComputationBridge and homogeneous_minimizes_cost in HorizonProblem rely upon for sigma-conserving strategic interaction. It operationalizes the Recognition Composition Law inside game theory by showing that the VCG payment rule internalizes the externality that would otherwise violate ledger balance. It leaves open the extension to combinatorial settings while preserving the same conservation property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.