← All papers
First page of Coercive at the equilibrium, monotone nowhere: exact convergence certificates for learning in first-price auctions

Coercive at the equilibrium, monotone nowhere: exact convergence certificates for learning in first-price auctions

Benjamin Lubin

cs.GT Nov 3, 2026 · v1
Exact identities and leading-order inequalities about the first-price auction operator are machine-checked in Lean 4 with Mathlib, in a released lean/FirstPriceCertificates development.
The Bayes-Nash equilibria of an auction are the solutions of a variational inequality, and for standard auctions its operator fails every monotonicity notion, so the theory of monotone operators is unavailable to learning in auctions. We show what replaces monotonicity for the first-price auction: a certificate that is strong but local. For uniform values the single-population operator has an exact closed form and an exact Minty identity at the equilibrium; for two bidders its Gateaux derivative there is $L^2$-coercive with best constant exactly one in every piecewise-linear bid space with $m$ pieces, while the Minty inequality holds only on a ball whose radius decays like $m^{-5/2}$. The decay is exact: $m^{5/2}$ times the radius converges to $1/(8 \cdot 3^{1/4})$, and the worst perturbations converge to an alternating geometric profile with ratio $-(2-\sqrt{3})$. Refinement shrinks the ball, not the constant; independent learners see the same constant. For a general prior and bidder count there are two certificates, at the true equilibrium and at the equilibrium of the finite-dimensional bid space a learning algorithm runs in. The first is an explicit weight $w_F$, positive for every log-concave prior, equal to the second exactly for the value distributions $F(v)=v^a$. Otherwise the learners' certificate differs by knot masses, because the discretized equilibrium's slopes oscillate with a law proved for two and three bidders, and for four under a computer-verified bottom layer. The limit of the learners' certificate is proved in closed form, a function of the prior alone, and characterizes positivity: positive uniformly in $m$ in the limit exactly when that minimum is positive, with a known rate; for one prior at every $m$ by interval arithmetic. For more bidders the limit is conjectured. The exact identities and leading-order inequalities are machine-checked in Lean.

The variational-inequality operator whose solutions are Bayes–Nash equilibria of first-price auctions is not monotone in any sense. Standard convergence theory therefore cannot certify that learning bidders reach equilibrium.

For uniform values the paper derives a closed-form single-population field and an exact Minty identity, then analyzes the Gateaux derivative at equilibrium in piecewise-linear bid spaces with m pieces. It extends the analysis to independent learners and to general priors, using an explicit weight w_F and knot-mass corrections arising from the discretized equilibrium's oscillating slopes. Interval arithmetic and computer verification support some steps. Exact identities and leading-order inequalities are machine-checked in Lean 4 over Mathlib.

For two bidders the derivative is L^2-coercive with best constant exactly one in every piecewise-linear space. The Minty inequality holds only on a ball whose radius decays like m^{-5/2}, and m^{5/2} times the radius converges to 1/(8·3^{1/4}). For general priors a closed-form limit of the learners' certificate characterizes positivity: proved for two and three bidders, for four under a computer-verified bottom layer, and conjectured for more.