pivot_identity
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.