Lean declarations

def Auction.FirstPrice.winner EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.FirstPrice
```
noncomputable def winner (b : I → U) : I := Auction.argmaxBid b
```

def Auction.FirstPrice.utility EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.FirstPrice

noncomputable def utility (v b : I → U) (i : I) : U :=
  if i = winner b then v i - b i else 0

lemma Auction.FirstPrice.utility_winner EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.FirstPrice
If `i` is the winner, utility is `v i − b i`.
```
lemma utility_winner {b : I → U} {i : I} (h : i = winner b) :
    utility v b i = v i - b i
```
lemma Auction.FirstPrice.utility_loser EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.FirstPrice
If `i` is not the winner, utility is `0`.
```
lemma utility_loser {b : I → U} {i : I} (h : i ≠ winner b) :
    utility v b i = 0
```

def Auction.FirstPrice.mechanism EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.FirstPrice

noncomputable def mechanism : MechanismWithTransfers I (fun _ => U) I U where
  allocationRule b := winner b
  paymentRule b i := if i = winner b then b i else 0

def Auction.FirstPrice.game EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.FirstPrice

noncomputable def game (v : I → U) : StrategicGame I U where
  strategy := fun _ => U
  payoff b i := utility v b i

lemma Auction.FirstPrice.game_eq_toStrategicGame EconCSLib @ cef01c7, EconCSLib.MechanismDesign.Auction.FirstPrice

lemma game_eq_toStrategicGame (v : I → U) :
    game v = mechanism.toStrategicGame
      (fun (w : I) (pay : I → U) (vals : I → U) (i : I) => if i = w then vals i - pay i else 0)
      v

Modules: EconCSLib.MechanismDesign.Auction.FirstPrice

First-Price Mechanism

The first-price (pay-your-bid) auction is a sealed-bid single-item mechanism in which the highest bidder wins and pays their own bid. All other bidders pay nothing.

Setup

Fix a finite, nontrivial bidder set I and an ordered abelian group U of bids and utilities. The bid profile is b : I → U.

winner b : I — the highest bidder, defined as Auction.argmaxBid b. The same deterministic tie-breaker as in the second-price auction ([[mechanism_design.auction.basic.ordered_bid_utilities]]).
utility v b i : U — quasi-linear payoff at valuation profile v: $$ u_i(v, b) \;=\; \begin{cases} v_i - b_i & i = \mathrm{winner}(b),\\ 0 & \text{otherwise}.\end{cases} $$

Mechanism and strategic-game packaging

mechanism : MechanismWithTransfers I (fun _ => U) I U packages the first-price auction as a transfer mechanism ([[mechanism_design.transfer.mechanisms_with_transfers]]). The report type is U per bidder, the allocation type is I (the winning bidder), and the payment rule is paymentRule b w = if w = winner b then b w else 0.
game v : StrategicGame I U packages the same auction as a strategic game with the bid profile as the strategy profile and the quasi-linear payoff above as the utility function.
game_eq_toStrategicGame certifies that game v agrees with mechanism.toStrategicGame for the auction utility function.

Allocation rule is shared with second-price

The first-price and second-price auctions share the same allocation rule (highest bidder wins, ties broken by argmaxBid); they differ only in the payment rule. This is the elementary instance of the broader observation that, within the single-parameter Myerson framework ([[mechanism_design.transfer.single_parameter_transfer_layer]]), allocation and payment are independent design choices.

Position in the library

The negative DSIC result is in the companion theorem node [[mechanism_design.auction.basic.first_price_no_dsic]]: truthful bidding is not weakly dominant in the first-price auction. Symmetric Bayesian Nash equilibria under IPV — the standard positive analysis of first-price — are tracked at the blueprint level in [[mechanism_design.auction.bayesian.symmetric_first_price_equilibrium]].

References

[AGT, Chapter 1, Section 1.3.2] Nisan, Roughgarden, Tardos, and Vazirani, Algorithmic Game Theory. First-price auction in the basic algorithmic game theory introduction.
[MFoGT, Chapter 12] Maschler, Solan, and Zamir, Game Theory. First-price auctions with private values.
[Krishna, Chapter 2, Section 2.3] Vijay Krishna, Auction Theory, 2nd ed.. First-price sealed-bid auction formulation and equilibrium analysis.