pivot_identity
The pivot identity asserts that in the two-agent single-item VCG auction the winner's payment equals the loser's bid, which is the externality imposed on the displaced agent. Mechanism designers cite it as the Clarke pivot rule that closes the incentive-compatibility argument for truthful reporting. The proof is a direct term-mode case split: assume the comparison, unfold the relevant payment definition, and rewrite with the if-branch that matches the assumption.
claimFor real numbers $v_0, v_1$, if $v_0$ is the higher bid then the winner (agent 0) pays exactly $v_1$, and if $v_1$ is the higher bid then the winner (agent 1) pays exactly $v_0$.
background
The module constructs a single-item VCG auction for two agents. Each agent $i$ has private valuation $v_i$ and submits bid $b_i$. The item is awarded to the higher bidder; the winner pays the second-highest bid while the loser pays zero. This payment rule is encoded in the sibling definitions payment₀ and payment₁, which are conditional on the comparison of bids. The local setting is Track E10, which replaces an earlier stub with a concrete mechanism whose dominant-strategy incentive compatibility is proved over the full real bid space.
proof idea
The term proof opens with refine to produce the two conjuncts. The first conjunct assumes $v_0 ≥ v_1$, unfolds payment₀, and rewrites with the positive if-branch. The second assumes $v_0 < v_1$, unfolds payment₁, and rewrites with the negative if-branch obtained via linarith on the strict inequality.
why it matters in Recognition Science
The identity supplies the fourth clause of the VCGCert structure and appears directly in the one-statement theorem vcg_one_statement. It encodes the σ-conservation property for the single-item case: the payment extracted equals the social-welfare externality. Within the Recognition framework it supplies the concrete payment rule needed to link the auction to the σ-cost ledger and to the dominant-strategy results that follow.
scope and limits
- Does not treat auctions with three or more agents.
- Does not enforce non-negativity of bids or valuations inside the statement.
- Does not address multi-item or combinatorial allocation rules.
- Does not derive the full DSIC inequalities, only the payment identity itself.
Lean usage
def vcgCert : VCGCert where ... pivot_identity := pivot_identityformal statement (Lean)
199theorem pivot_identity (v₀ v₁ : ℝ) :
200 -- If agent 0 wins (v₀ ≥ v₁), they pay v₁.
201 (v₀ ≥ v₁ → payment₀ v₀ v₁ = v₁) ∧
202 -- If agent 1 wins (v₀ < v₁), they pay v₀.
203 (v₀ < v₁ → payment₁ v₀ v₁ = v₀) := by
proof body
Term-mode proof.
204 refine ⟨?_, ?_⟩
205 · intro h
206 unfold payment₀
207 rw [if_pos h]
208 · intro h
209 unfold payment₁
210 rw [if_neg (by linarith)]
211
212/-- **σ-CONSERVATION (single-item case).** Under truthful bidding, the
213total surplus on the utility ledger (winner's utility) plus the
214payment equals the winner's valuation. Equivalently: the auction
215extracts a payment exactly equal to the social-welfare externality. -/