sigma_cost_to_agent_0
plain-language theorem explainer
Game theorists cite this definition when proving VCG payments equal externality costs in σ-conserving auctions. It sets the σ-cost imposed on agent 1 by allocating the item to agent 0 equal to agent 1's valuation v₁. This captures the utility the displaced agent loses in the counterfactual where agent 0 is absent. The definition follows directly from the auction payment rule with no lemmas required.
Claim. The σ-cost of allocating the item to agent 0 given agent 1's valuation $v_1$ equals $v_1$.
background
The module builds a single-item VCG auction for n agents. The item goes to the highest bidder; the winner pays the second-highest bid while losers pay zero. This payment equals the externality imposed on the displaced agent. The σ-cost term measures that lost utility in the counterfactual where the winner is removed. Upstream cost functions come from J-cost of recognition events, as defined in ObserverForcing.cost and MultiplicativeRecognizerL4.cost, and from structures in PhiForcingDerived and SpectralEmergence.
proof idea
The declaration is a direct definition that sets the σ-cost equal to the input valuation v₁. It functions as a one-line wrapper that identifies the cost with the counterfactual utility loss for the displaced agent.
why it matters
This definition is used inside VCGCert to certify dominant-strategy incentive compatibility for both agents and inside the theorem that equates VCG payments to σ-costs. It supplies the concrete cost term required for the σ-conserving auction track. The construction connects the mechanism to the Recognition framework through conservation properties that rest on the Recognition Composition Law and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.