∎Carlos Toledo
mfg-cap · validated numerics · every bound computed in interval arithmetic, live

A mean-field game equilibrium, enclosed in your browser.

This page does not solve the equations and show you the answer. It solves them, then proves the answer: a radii-polynomial contraction argument in the weighted algebra ℓ¹ν (ν > 1, analytic tail), every inequality evaluated in outward-rounded interval arithmetic, returning either a refusal or an explicit ball that contains an exact classical solution. When the coupling is monotone (c > 0), that ball carries local uniqueness in the even subspace the enclosure is built in. When c < 0, anti-monotone coupling admits a circle of translates — the page still encloses a solution, and it does not claim uniqueness there. Move any control and the proof is redone from scratch.

−σ u″ + ½(u′)² + ρ = c·m + V(x)HJB · the value
−σ m″ − (m u′)′ = 0Fokker–Planck · the crowd
∫m = 1  ·  ∫u = 0  ·  m > 0normalisation · certified, not assumed

The proof recomputed on every change

verdict
—
enclosure radius r
—
ergodic constant ρ
—
certified min m
—
Y₀ (defect)
—
Z₁ (contraction)
—
The verdict is gated on the whole argument, not on the residual: the Newton residual being small is what suggests a solution is near, and proves nothing. What proves it is Z₁ < 1 (the approximate inverse really is one) together with a radius at which the radii polynomial is strictly negative — verified in interval arithmetic, not in floating point. Positivity of the density is certified over the entire ball, never assumed.

The enclosed solution value and density

Oxblood: the value function u. Teal: the population density m. The enclosure radius is far below a pixel at these settings — which is the honest situation, and the reason the radius is printed as a number rather than drawn as a band.

The radii polynomial p(r) < 0 is the proof

p(r) = ½Z₂r² − (1−Z₁)r + Y₀. Where the curve dips below zero, the map is a contraction on that ball. Amber marks the reported radius. If the curve never crosses, there is no proof — and the page says so instead of showing you a solution.

Where uniqueness theory is silent — and the machine is not

For c > 0 the coupling is increasing: Lasry–Lions monotonicity applies and the solution is unique, classically. For c < 0 it does not apply at all. Past c* = −σ²(2π)² a branch bifurcates from the constant state, and there are at least three solutions at the same parameters. Certifying two of them in disjoint balls is a proof of non-uniqueness — a statement about the equations, not about a solver.

Multiplicity, by disjoint enclosure two solutions at identical parameters

The curve is the bifurcation diagram: amplitude of the non-constant branch against c, with the constant state along zero. Dots are points where both solutions have been certified and their balls shown disjoint. At the bifurcation point itself the linearisation is singular, so no enclosure can exist and the proof refuses — a verifier that succeeded there would be broken.

What this does not show

“Proved” in the mathematician’s sense — never here. Rung 5 of this project’s evidence ladder requires a proof document with a named human reviewer, a date and a signature; there is no agent path to it, and none is asserted anywhere in this file. Rung 4, certified, requires a ledger certificate record, and the ledger holds no record for this system at all — every claim and certificate on file is about the congestion game, at other parameters. Both ladder words are therefore deliberately absent here as a status; the compound noun computer-assisted proof and the verbs prove and certify still appear below for the mechanism — a contraction argument, a certificate — which is the product and is not a status. What this page carries is a computer-assisted proof: a machine-checked enclosure, backed by a mutation-tested battery (tests/test-cap.js — 17 checks and 6 falsifiers; revert a check and it goes red). That is what it claims and all it claims.

This is not a new existence or uniqueness theorem. For c > 0 both are classical (Lasry–Lions). The contribution is the enclosure — an explicit, machine-checked ball with a certified ergodic constant and a certified positive density — and the multiplicity result in the regime where the classical theory makes no claim.

standard The machinery is standard and the citations are owed. Newton–Kantorovich in radii-polynomial form is the van den Berg–Lessard framework; the nearest computer-assisted proof on the reduced equation is Ayala, García-Azpeitia & Lessard on gap solitons in Bose–Einstein condensates (2026). The Hopf–Cole reduction of this MFG system is textbook (Cirant 2015; Cirant–Verzini 2017; Ullmo–Swiecicki–Gobron 2019) and is used here only as an independent cross-check, never as the route of proof.

open The open item, stated first rather than last: every instance certified here has a quadratic Hamiltonian, for which a scalar reduction exists. Until a non-quadratic Hamiltonian, two populations, or congestion is certified, the system method has not been shown to do anything the scalar method could not.

The conjecture that motivated this was mis-posed, and that is part of the result. The idea was that monotonicity would supply the inverse bound coercivity supplies elsewhere. In fact a computation needs neither: it needs an approximate inverse whose defect is small, obtained by construction. That is exactly why this page can certify solutions in the anti-monotone regime.

Companion artifacts, same certificate standard: the MFG Lab and the SIN-MFG note.
mfg-cap · MIT licensed · no libraries, no build step, no precomputed data — the proof above runs here.
The page is generated from the kernels, and a gate asserts the copies are byte-identical, so what runs in this browser is what make check runs headlessly: 17 checks and 6 falsifiers, including the parity bug that once made the Fourier residual machine-zero at a point that did not solve the PDE.