The prior proof (mfg-cap) certified a mean-field game with a quadratic Hamiltonian — which Hopf–Cole-reduces to a Gross–Pitaevskii ground state, so a referee can call it “GP in disguise.” This page reports the sequel: a game with congestion, ½(u′)²/ma, which has no such reduction. The mathematics is real and the certificate mechanism below runs live; the congestion instance is now enclosed — existence, local uniqueness in the full ℓ¹ν (even+odd) ball (Stage 2.2), and a strictly positive density, within r ≈ 7.75e−15.
We report what is, to our knowledge, the first validated-numerics enclosure of an equilibrium for a mean-field game with congestion. A Newton–Kantorovich / radii-polynomial argument in outward-rounded interval arithmetic returns, from a numerical candidate, an exact solution (u, m) within an explicit distance r, locally unique in the full ℓ¹ν (even+odd) ball, with strictly positive density, for the discounted Gomes–Mitake system (no ergodic constant). The half-integer power (a = ½) is handled by adjoining s = m1/2 and w = m−1/2 via the polynomial constraints s∗s=m, s∗w=1, so the certificate rests on a uniform positive lower bound mmin>0 over the whole validation ball. Local uniqueness is machine-checked in the full space (Stage 2.2): Φ preserves parity at this instance (γ > 0, V even in x), so DΦ is block-diagonal on even ⊕ odd Fourier modes; Y₀ is unchanged (the candidate is even) and one extra Z₁odd bound closes with Z₁ = max(Z₁even, Z₁odd) ≈ 0.5268 < 1 (both blocks dominated by the same analytic-tail column). The candidate itself is still solved in the even (cosine) subspace — that is a search convenience, not the uniqueness claim. Gomes–Mitake monotone uniqueness (NoDEA 22 (2015) 1897–1910; arXiv:1407.8267) remains the continuum backdrop; what is new here is the enclosure of the local ball, not a re-derivation of their theorem. We are explicit about the boundary of validity: the proof closes in the moderate regime and refuses as the density concentrates — and where it refuses is reported honestly (its full map A⋆(σ,a) is future work).
The enclosure is not a finite truncation with unquantified projection error. Unknowns are Fourier coefficients in the weighted sequence Banach algebra ℓ¹ν (ν = 1.05 > 1). Y₀ is exact by band-limitation of the candidate; Z₁ carries a closed-form analytic tail over infinitely many columns beyond the inverted block of size N. With ν > 1 the geometric decay of the weights forces the enclosed zero to be a real-analytic function of x — hence a classical solution of the PDE on the torus, not merely a Galerkin approximation. N is the size of the inverted block, not a truncation dimension. The printed existence radius r ≈ 7.75e−15 is the smallest radius at which the radii polynomial closes; local uniqueness for the contraction argument holds on the whole admissible window up to min(rMax, rCap) with rCap = 1e−2 (twelve orders larger than the existence radius). Reporting only the tiny r as “the” uniqueness radius understates what the certificate already proves. Full even+odd local uniqueness at that radius is mutation-tested (Stage 2.2: Z₁ = max(Z₁even, Z₁odd)).
A radii polynomial p(r) = ½Z₂r² − (1−Z₁)r + Y₀. Where it dips
strictly below zero, the map T = x − A·F is a contraction on that ball and has exactly one fixed point there
— an exact solution. This driver is ported faithfully from eqcert/src/radii.js, including the cancellation-stable
root and the refusal cases. In the battery Y₀, Z₁, Z₂ come from a real solve and every inequality is
evaluated in outward-rounded intervals; here they are set live.
Congestion’s difficulty, shown here in its classical form: a reciprocal w=1/ma blows as m→0, and bounds can carry a factor up to 1/mmina+1. The shipped certificate does not put that factor in Z₂ — auxiliaries s≈√m, w≈1/√m keep the system polynomial; positivity is two walls (min m and min w) over the ball. Either way, the concentrated regime is where the proof must refuse. Slide r up (or the candidate floor down) and watch the wall arrive. mmin = m̄₀ − r is a genuine (conservative) certified lower bound; in the battery m̄₀ and r come from a real enclosure, here they are set live.
The discounted Gomes–Mitake congestion instance (a = ½, σ = 0.5, A = 0.3, γ = 0.5, N = 14), enclosed in outward-rounded interval arithmetic by the validation kernel and gated by its battery.
| σ | a | γ | N | radius r | certified min m | Z₁ |
|---|---|---|---|---|---|---|
| 0.5 | 1/2 | 0.5 | 14 | 7.75e−15 | 0.9736 | 0.5268 |
Every check above runs through the same apparatus — the radii polynomials, the interval library, the pointwise witnesses. Code that is shared can be wrong together. So here is one that shares none of it. Test the HJB against (m−1), the Fokker–Planck equation against u, and subtract. The σu″ and σm″ terms coincide after two integrations by parts and cancel, so what is left does not depend on σ at all:
−½ ∫ (u′)² m−a(m+1) = A ∫ cos(2πx) m + γ (∫m² − 1) (†)
The left side cannot be positive. With ∫m = 1 — which the Fokker–Planck equation derives, we never impose it — that forces ∫m² ≤ 1 + |A|/γ. An a priori bound on the density, with no ‖V‖∞ anywhere in it. That is the estimate Gomes–Mitake’s hypothesis (A2) exists to supply, arriving instead from the monotone structure of the coupling itself.
Measured on the solver’s output, on a 4096-point quadrature independent of the solve grid, (†) closes to a relative residual of 7.4e−14, 1.8e−13, 1.6e−13 and 4.7e−14 at γ = 0.3, 0.5, 0.9, 1.5 — with ∫m = 1 holding to 1e−15 and the bound holding at each.
The numbers above are not ours to assert. Download the verifier, run it on your own machine, and watch the certificate close — or refuse if you tamper with it.
python3 verify_congest.py — no dependencies, one file (it uses math.nextafter for
outward-directed rounding). It carries the certified candidate + the checker, not the solver, independently recomputes
Y₀, the even-block Z₁, Z₂, the radius r, both positivity walls and all seven falsifiers in interval arithmetic, and prints
CONGEST CAP: VERIFIED. Perturb a single candidate coefficient and it prints
REFUSED — a certificate that cannot go red is fake. Cross-checked bit-for-bit against the Node battery
that gates the same kernel. Scope, stated plainly: this standalone file certifies existence, positivity and
even-subspace local uniqueness, and says so in its own output. The odd-block Z₁ that upgrades uniqueness to the
full ℓ¹ν (even+odd) ball — Stage 2.2 above — is enclosed by the JS kernel and gated by its
battery, and has not yet been ported to this file; until it is, the full-space claim rests on one implementation.
Four badges, no blurring between them — and each names a MECHANISM, never a status this project awards itself. (The first read gated until 2026-07-29: same meaning, but the word collided with the site's Open/Gated access tiers and inverted their sense, and to an outside reader it says you cannot see this rather than a battery checks this.) mutation-tested — a headless battery in this repo checks it and is mutation-tested (revert the check, it goes red); standard — off-the-shelf or cited, not re-derived; prospective — pre-registered, the shape of the claim fixed in advance but the number not yet computed; open — the honest frontier, known and not done. This page reports a completed enclosure: the kernel is built and mutation-tested (revert a check, it goes red), so every congestion-result row below is mutation-tested. Only the honest frontier — the concentrated regime and the refusal map A⋆(σ,a) — stays open. Deliberately absent: the words proved and certified as a status. Both are rungs on this project's evidence ladder — rung 5 needs a named human signature, rung 4 needs a ledger certificate record — and no such record covers this instance (σ=0.5, A=0.3, γ=0.5, N=14). What backs every row below is a mutation-tested battery, which is what mutation-tested says and all it says.
| claim | status | what backs it |
|---|---|---|
| The radii-polynomial contraction argument | standard | Banach fixed point / van den Berg–Lessard; ported from eqcert, live above |
| The validation pipeline produces a real enclosure (de-risked on the quartic MFG: r ≈ 8e−15, min m ≈ 0.90) | mutation-tested | kernel/validate.js + tests/test-validate.js (interval arithmetic; 6 falsifiers red) |
| Half-integer powers m±1/2 as auxiliary polynomial unknowns (s∗s=m, s∗w=1) | standard | Lessard–Mireles James–Ransford, Physica D 334 (2016) |
| a = 1 collapses to a scalar ODE (u = σ(1−m)) — so the target is a ∈ (0,1), a = ½ | mutation-tested | tests/test-reduction.js, 5 checks |
| Discounted-congestion pre-commit gates (min m ≈ 0.97, σmin(DF) bounded, ∫m=1) | mutation-tested | tests/gate-discounted.js — both PASS, build with γ>0 |
| Congestion has no Hopf–Cole / GP reduction (at a = ½) | standard | structural; no NLS analog of a density-dependent Hamiltonian |
| A validated-numerics enclosure of a congestion MFG solution — to our knowledge the first | mutation-tested | the enclosure is battery-checked (r ≈ 7.75e−15, all falsifiers red); “first” rests on an occupancy search that found no prior MFG CAP — a search negative, not machine-checked |
| Existence, local uniqueness in the full ℓ¹ν (even+odd) ball, positivity of (u, m) at the discounted a = ½ instance | mutation-tested | validation kernel: r ≈ 7.75e−15, min m ≥ 0.9736, min w ≥ 0.987; three witnesses agree; Stage 2.2 Z₁ = max(Z₁even, Z₁odd) ≈ 0.5268 |
| Full even+odd local uniqueness at r ≈ 7.75e−15 | mutation-tested | Stage 2.2: Φ preserves parity ⇒ DΦ block-diagonal ⇒ Y₀ unchanged. Odd-block Z₁ enclosed with the same approximate-inverse + analytic-tail structure as the even block (Z₁odd = Z₁even = 0.5267562117334962 at A=0.3; both worst columns tail(analytic)). Radii polynomial consumes Z₁ = max(Z₁even, Z₁odd). Gated by the congestion validate battery P1b/D1b |
| Ergodic form collapses to a scalar ODE for every a ∈ (0,1] — so the target is the DISCOUNTED system | mutation-tested | tests/test-reduction.js, 5 checks; workflow reduction agent |
| The a = ½ augmented-system algebra (the equations above) | mutation-tested | DΦ checked against finite differences (test D1) and the enclosure closes on it (validation battery) |
| Concentrated / near-vacuum regime, and the endpoints a → 0, 1 | open | the reciprocal bound diverges as mmin→0 — the honest frontier |
Not a new existence theorem. Congestion existence is the Gomes school's analytic program — for a ∈ [0,1), Gomes–Mitake (NoDEA 2015, Thm 1.1), of the discounted system, with uniqueness besides when V is strictly increasing in m. The contribution is the enclosure — a machine-checked ball around (u, m) with a certified positive density. It is additive to that program, not a re-derivation.
And a correction we owe, found 2026-08-04 by reading the paper we had been citing. An earlier version of this page said the instance certified here is one that Gomes–Mitake’s continuation argument “guarantees only abstractly.” That was wrong. Their hypothesis (A2) requires V globally bounded with bounded derivatives, and every a priori estimate in their §2 carries ‖V‖∞ in its constant. Our V = A cos 2πx + γm is not bounded, so Theorem 1.1 does not apply to this instance at all. That is not a gap in the existence theory either, and we do not present it as one: (A2) exists to produce a priori bounds, and the Lasry–Lions monotone structure produces one of its own — see the identity below, which forces ∫m² ≤ 1 + |A|/γ with no ‖V‖∞ in the constant. We expect existence here to be reachable by adapting their argument with that estimate in place of theirs, and claim no priority over such a result.
The machinery is standard and the citations are owed. Radii-polynomial validation has been native to systems since Day–Lessard–Mischaikow (SIAM J. Numer. Anal. 45(4) 1398–1424, 2007) and has never required a scalar reduction; non-polynomial nonlinearities are handled by Breden (arXiv:2102.01501); coupled elliptic pairs on the torus by Breden–Kuehn–Soresina (arXiv:1704.03827) and Breden–Payan (arXiv:2311.13896). An expert assembling those three would reach much of what is here. The reciprocal trick is Lessard–Mireles James–Ransford and Hungria–Lessard–Mireles James (2016); the nearest congestion treatment, Nurbekyan (arXiv:1703.03954), is analytical, not a computer-assisted proof. The absence of a Hopf–Cole reduction says this result is not a corollary of the Gross–Pitaevskii computer-assisted proofs — it does not say the method is new, and we do not claim it is.
Local uniqueness is full-space; the candidate search is not. The numerical candidate is still solved in the even (cosine) subspace — a search convenience under γ > 0. Stage 2.2 then encloses the odd block of DΦ with one extra Z₁ bound, so the radii-polynomial uniqueness statement is machine-checked in the full ℓ¹ν ball. Continuum uniqueness for the PDE itself remains Gomes–Mitake’s theorem, not ours.
The scope is bounded, and stated first. Exponent a = ½ (a non-integer in (0,1) — a = 1 collapses to a scalar ODE, a = 2 is supercritical), moderate congestion, density off vacuum. The concentrated / near-vacuum regime is open (the wall panel shows why). No claim depends on it.
Instance choice is a hard rule. We will not certify a 1D instance for which the Gomes group has an explicit solution — a CAP there looks trivial. The certified instance must be one their analysis leaves non-constructive, and the paper will say why it is.
To our knowledge the first validated-numerics enclosure of a stationary mean-field game with congestion — the density-dependent Hamiltonian ½(u′)²/√m that no Hopf–Cole reduction reaches. Existence, local uniqueness in the full ℓ¹ν (even+odd) ball (Stage 2.2), and a strictly positive density are enclosed in outward-rounded interval arithmetic (r ≈ 7.75e−15, min m ≥ 0.9736, min w ≥ 0.987); every check is mutation-tested; the whole page is one file — no libraries, no build step, no network. One instance, self-reviewed — no external referee yet, and the refusal map A⋆(σ,a) is future work. Sequel to mfg-cap (the quadratic case), same certificate standard.
Carlos Toledo builds computer-assisted proofs for mean-field games and network equilibria. Where a paper reports a converged iterate, these notes return a certificate — an exact-rational or interval enclosure of the equilibrium, with its location and local uniqueness certified, or an explicit refusal where the instance is degenerate. Certificates over tolerances; a falsifier behind every claim; a green run is evidence precisely because a broken one is built to go red.
For a research group this is a way to validate and stress-test a published result — independently, and in good faith. The same machinery certifies numerical and optimization claims — the kind a frontier system must be able to depend on rather than merely hope for.
Carlos Toledo · carlos@carlostoledo.co · on the open-source eqcert certification kernel (MIT) · 2026
Licence. This page — its text, figures, tables and layout — is licensed CC‑BY 4.0: share and adapt it, with credit to Carlos Toledo and an indication of changes. The verifier it carries (verify_congest.py) is MIT, not CC‑BY — as is the eqcert kernel it is ported from; the full MIT text and its copyright notice travel inside the downloaded file, so the file is self-sufficient once it leaves this page. The solver that produced the certified candidate is not published and is not licensed here. Full terms: technical-reports/LICENSE.md.