dsic_agent_one
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend to auctions with three or more agents.
- Does not address multi-unit or combinatorial settings.
- Does not incorporate reserve prices or modified payment rules.
- Does not prove revenue or efficiency properties beyond incentive compatibility.
Lean usage
dsic_agent_one v₁ v₀formal statement (Lean)
171theorem dsic_agent_one (v₁ b₀ : ℝ) (b₁' : ℝ) :
172 utility₁ v₁ b₀ b₁' ≤ utility₁ v₁ b₀ v₁ := by
proof body
Term-mode proof.
173 unfold utility₁
174 by_cases h_truth : b₀ ≥ v₁
175 · -- Truthful: agent 1 loses (since b₀ ≥ v₁), utility = 0.
176 rw [if_pos h_truth]
177 by_cases h_dev : b₀ ≥ b₁'
178 · -- Deviation also loses, utility = 0.
179 rw [if_pos h_dev]
180 · -- Deviation wins (b₁' > b₀), utility = v₁ - b₀.
181 -- Since v₁ ≤ b₀, we get utility ≤ 0.
182 rw [if_neg h_dev]
183 linarith
184 · -- Truthful: agent 1 wins (since v₁ > b₀), utility = v₁ - b₀ > 0.
185 rw [if_neg h_truth]
186 by_cases h_dev : b₀ ≥ b₁'
187 · -- Deviation loses, utility = 0 ≤ v₁ - b₀.
188 rw [if_pos h_dev]
189 push_neg at h_truth
190 linarith
191 · -- Deviation also wins, utility = v₁ - b₀ (same).
192 rw [if_neg h_dev]
193
194/-! ## §4. The pivot identity and σ-conservation -/
195
196/-- **PIVOT IDENTITY.** Under truthful bidding, the winner's payment
197equals the loser's valuation: the externality the winner imposes on
198the displaced agent. -/