dsic_agent_one
plain-language theorem explainer
Agent 1 in the two-agent second-price auction obtains weakly higher utility by bidding its true valuation v₁ than by any deviation b₁', for any fixed opposing bid b₀. Mechanism designers cite the result to confirm dominant-strategy incentive compatibility of the VCG mechanism. The proof executes exhaustive case analysis on whether the truthful bid wins and whether the deviation wins, reducing each of the four branches to a linear inequality after rewriting the conditional utility definition.
Claim. For all real numbers $v_1, b_0, b_1'$, the utility of agent 1 with valuation $v_1$ when bidding $b_1'$ against bid $b_0$ is at most its utility when bidding truthfully $v_1$, where utility equals $v_1 - b_0$ if the bid strictly exceeds $b_0$ (item awarded, paying the second-highest bid) and equals 0 otherwise (ties broken in favor of agent 0).
background
The module builds the canonical two-agent single-item VCG auction: the item is awarded to the highest bidder with ties resolved to agent 0; the winner pays the second-highest bid while losers pay zero. Agent 1's utility is therefore $v_1 - b_0$ precisely when its bid exceeds $b_0$ and zero otherwise; this is the explicit definition of the sibling utility₁ that the proof unfolds. The surrounding development imports the identity event (J-cost minimum at state 1) from ObserverForcing and vantage projections from VantageCategory, though neither is invoked directly. The local theoretical setting replaces an earlier stub that only verified the trivial zero-valuation case with a full proof of dominant-strategy incentive compatibility over the entire real bid space.
proof idea
Unfold utility₁ to expose the if-expression. Split on the predicate b₀ ≥ v₁ (truthful win/lose status) and, inside each arm, split on b₀ ≥ b₁' (deviation win/lose status). Rewrite the corresponding if-branches. The four resulting inequalities compare either 0 with 0, 0 with v₁ - b₀ ≤ 0, or v₁ - b₀ with itself; each is discharged by linarith.
why it matters
The lemma supplies the second half of the DSIC property and is invoked by truthful_is_nash to conclude that truthful bidding forms a Nash equilibrium. It also populates the vcgCert record and appears inside the master vcg_one_statement theorem. Within the Recognition framework it demonstrates that the second-price mechanism is σ-conserving: the winner's payment exactly equals the externality (loser's valuation) imposed on the displaced agent, matching the pivot identity. It discharges the scaffolding left by the prior stub restricted to the zero-bid branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.