abbrev
definition
def or abbrev
BidVector
show as:
view Lean formalization →
formal statement (Lean)
104abbrev BidVector (n : ℕ) := Fin n → ℝ
proof body
Definition body.
105
106/-! ## §2. Two-agent VCG (the cleanest non-trivial case)
107
108We prove DSIC in full for two agents. The argument generalizes
109immediately to `n` agents (the runner-up is just the second-highest
110bid in `Finset.image b Finset.univ.erase i*`), but two agents capture
111the σ-conservation structure with no combinatorial overhead.
112
113Agent 0 vs. Agent 1. Each has a private valuation `v₀, v₁ ≥ 0` and
114submits a bid `b₀, b₁ ∈ ℝ`. The high bidder wins (ties broken
115arbitrarily — we break to agent 0). The winner pays the loser's bid;
116the loser pays nothing.
117-/
118
119/-- The winner under bid pair `(b₀, b₁)`. Returns `0` if `b₀ ≥ b₁`,
120else `1`. -/