truthful_is_nash
plain-language theorem explainer
Truthful bidding forms a Nash equilibrium in the two-agent single-item VCG auction: neither agent improves utility by unilaterally deviating from their true valuation when the other bids truthfully. Mechanism designers in Recognition Science cite the result to confirm that sigma-cost payments inherit the incentive alignment of classical VCG. The proof is a one-line wrapper that pairs the dominant-strategy incentive-compatibility statements already shown for each agent.
Claim. In the two-agent VCG auction with valuations $v_0, v_1 : ℝ$, truthful bidding is a Nash equilibrium when $∀ b_0' : ℝ, u_0(v_0, b_0', v_1) ≤ u_0(v_0, v_0, v_1)$ and $∀ b_1' : ℝ, u_1(v_1, v_0, b_1') ≤ u_1(v_1, v_0, v_1)$, where $u_i$ is the utility of agent $i$ (valuation minus VCG payment if winner, zero otherwise).
background
The module defines a single-item VCG auction for two agents. Each agent $i$ holds private valuation $v_i$ and submits bid $b_i$. The highest bidder wins the item and pays the second-highest bid; losers pay zero. Utility for agent $i$ is therefore $v_i$ minus payment when winning and zero when losing. This payment rule is identified with the sigma-cost externality imposed on the displaced agent. The construction rests on the Agent structure (private preference and public vote) and on cost functions that return the J-cost of a recognition event. Upstream lemmas supply the multiplicative recognizer cost and the ledger factorization that calibrate these quantities to the Recognition Science framework.
proof idea
The proof is a one-line wrapper that applies dsic_agent_zero and dsic_agent_one. These two lemmas already establish that truthful reporting weakly dominates every deviation for agent 0 (given agent 1's truthful bid) and symmetrically for agent 1. Their conjunction directly yields the Nash condition.
why it matters
The theorem supplies the Nash-equilibrium clause inside the VCGCert structure, the master certificate for the sigma-conserving auction (Track E10). It completes the demonstration that the payment rule, defined as the sigma-cost externality, makes truthful reporting a stable strategy profile. The result sits downstream of the per-agent DSIC statements and feeds the overall mechanism-design certificate that links VCG to Recognition Science cost accounting. It touches the open question of extending the construction to $n>2$ agents while preserving sigma-conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.