vcg_one_statement
The theorem asserts dominant-strategy incentive compatibility for both agents, the pivot payment identity, and sigma-conservation of total surplus equaling social welfare in the two-agent Vickrey auction. Mechanism designers working inside recognition-based cost frameworks would cite it to connect incentive properties directly to sigma-cost balance. The proof is a one-line term that assembles four supporting lemmas on DSIC and conservation.
claimFor the single-item second-price auction with two agents having valuations $v_0, v_1$ and bids $b_0, b_1$, the mechanism satisfies: (1) dominant-strategy incentive compatibility, so each agent's utility is maximized by reporting its true valuation for any report of the other; (2) the winner's payment equals the loser's valuation; (3) the sum of both utilities plus payments equals the social welfare value $max(v_0, v_1)$.
background
The module builds a concrete single-item VCG auction for $n$ agents. The allocation rule awards the item to the highest bidder. The payment rule charges the winner the second-highest bid and charges losers zero. Agent utility is then valuation minus payment when winning and zero otherwise. Sigma-cost of an allocation to one agent is defined as the maximum valuation among the remaining agents, representing welfare lost by the displaced runner-up.
proof idea
The proof is a one-line term wrapper that directly packs the dominant-strategy incentive compatibility lemma for the first agent, the corresponding lemma for the second agent, the pivot identity lemma applied under the assumption that the first valuation is at least the second, and the sigma-conservation equality that holds when both agents report truthfully.
why it matters in Recognition Science
This declaration completes the core VCG construction in the sigma-conserving auction track by proving incentive compatibility over the unrestricted real bid space and linking payments to sigma-cost. It supplies the explicit four-part statement that replaces earlier trivial stubs. The module note records that the same case analysis extends to $n$ agents by substituting the runner-up bid for the second valuation, leaving the full $n$-agent formalization as the immediate open step.
scope and limits
- Does not prove the properties for auctions with more than two agents.
- Does not treat multi-item or combinatorial valuation settings.
- Does not incorporate computational limits on bid submission or verification.
- Does not establish uniqueness of this payment rule among all DSIC mechanisms.
formal statement (Lean)
358theorem vcg_one_statement :
359 -- (1) DSIC for agent 0.
360 (∀ (v₀ b₁ b₀' : ℝ), utility₀ v₀ b₀' b₁ ≤ utility₀ v₀ v₀ b₁) ∧
361 -- (2) DSIC for agent 1.
362 (∀ (v₁ b₀ b₁' : ℝ), utility₁ v₁ b₀ b₁' ≤ utility₁ v₁ b₀ v₁) ∧
363 -- (3) Pivot identity (when 0 wins).
364 (∀ (v₀ v₁ : ℝ), v₀ ≥ v₁ → payment₀ v₀ v₁ = v₁) ∧
365 -- (4) σ-conservation under truthful.
366 (∀ (v₀ v₁ : ℝ),
367 utility₀ v₀ v₀ v₁ + utility₁ v₁ v₀ v₁ +
368 (payment₀ v₀ v₁ + payment₁ v₀ v₁) = max v₀ v₁) :=
proof body
Term-mode proof.
369 ⟨dsic_agent_zero, dsic_agent_one,
370 fun v₀ v₁ h => (pivot_identity v₀ v₁).1 h,
371 sigma_conservation_truthful⟩
372
373end -- noncomputable section
374
375/-! ## §9. Note on the n-agent generalization
376
377For `n` agents, the same argument applies with the substitutions:
378
379- Winner = `argmax b_i`.
380- Payment by winner = `max_{j ≠ winner} b_j` (the second-highest bid).
381- σ-cost of allocating to `i` = `max_{j ≠ i} v_j` (welfare lost by displaced runner-up).
382
383The DSIC proof generalizes case-by-case (truthful wins/loses ×
384deviation wins/loses), with the runner-up bid replacing `v₁` / `b₁`
385in the two-agent argument.
386
387Done at `n = 2` here because that is where the σ-conservation