sigma_cost_to_agent_1
plain-language theorem explainer
sigma_cost_to_agent_1(v₀) defines the σ-cost imposed on agent 1 when the item is allocated to agent 1 as exactly the valuation v₀ of the displaced agent 0. Mechanism designers working on VCG auctions in the Recognition Science setting cite this when equating payments to externality costs. The definition is a direct one-line equality that supplies the missing term for the case where agent 1 wins.
Claim. Let $c_1(v_0)$ denote the σ-cost of allocating the item to agent 1 when agent 0 reports valuation $v_0$. Then $c_1(v_0) := v_0$.
background
The module builds a two-agent single-item VCG auction. Each agent reports a bid; the higher bidder wins and pays the lower bid (the externality imposed on the loser). The σ-cost is the recognition cost of that allocation, drawn from the J-cost construction in upstream results such as ObserverForcing.cost (cost of a recognition event) and MultiplicativeRecognizerL4.cost (derived cost on positive ratios). The module replaces earlier trivial stubs and works over the full bid space ℝ.
proof idea
Direct definition that sets sigma_cost_to_agent_1 v₀ to v₀. No lemmas or tactics are applied; the equality is the entire body.
why it matters
The definition supplies the second clause of vcg_payment_eq_sigma_cost, which equates VCG payments to σ-costs. It is referenced inside the VCGCert structure that certifies DSIC for both agents and truthful bidding as a Nash equilibrium. In the Recognition Science framework it completes the σ-conservation property for the VCG mechanism on Track E10.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.