Coercive at the equilibrium, monotone nowhere: exact convergence certificates for learning in first-price auctions
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.