Almulla, Ferreira and Gomes (Dynamic Games and Applications, 2017) solve a stationary mean-field game numerically and write, of the case with nonzero mean drift, "we are not aware of any closed-form solution." This page encloses that case: the whole game reduces, through its constant current, to two numbers, and the two numbers are enclosed in a Krawczyk box with every integral a rigorous quadrature. A classical solution exists, is locally unique, and its density is strictly positive — proved, not observed on a plot. The paper's own closed form, in the case that has one, is the certifier's control.
The system is the one-dimensional, first-order, stationary mean-field game of Almulla, Ferreira and Gomes (their equation (1.1)), on the torus:
First order: no viscosity, no Laplacian. The unknowns are the value function u, the density m and the constant H̄ that lets m carry unit mass. The paper builds two numerical methods for it — a gradient flow on the variational functional and a contracting monotone flow — and validates both against the explicit solutions it constructs in §2.1 for the case ∫b = 0, where u = 0 and m = e^V/∫e^V. Then, verbatim:
If ∫ b dx ≠ 0, we are not aware of any closed-form solution.Almulla, Ferreira & Gomes, §2.1
Their one example with nonzero mean drift is b = cos² 2πx (their Figures 7 and 8, the monotone flow on 100 grid points), with V = sin 2πx as everywhere in the paper. ∫b = ½. The figures are the only record of the answer: §4 carries no table, so there is nothing to reproduce to a printed digit, and the word for what follows is enclosure, never reproduction.
The transport equation says the flux m (u_x + b) has zero derivative on the torus, so it is a constant — the current j. This is the one-dimensional current formulation of Gomes, Nurbekyan and Prazeres; it is their method and it is cited as such. With u_x = j/m − b, the Hamilton–Jacobi equation becomes, at every point x, one scalar equation in m:
φ_j is strictly increasing on m > 0 (its derivative is 1/m + j²/m³), so for any pair (j, H̄) the density is the unique inverse m(x) = φ_j⁻¹(r(x)), smooth by the implicit function theorem. Two conditions remain, and they fix the two numbers:
When ∫b = 0 the second condition forces j = 0 and the first returns exactly the paper's closed form, H̄ = ln ∫e^V. When ∫b ≠ 0 it forces j ≠ 0, and the pair (j, H̄) is what the flow was hunting. A solution of the two equations rebuilds a classical solution of the whole system by construction: m from the inverse, u from ∫(j/m − b) with its mean removed, both equations satisfied pointwise. So enclosing the pair encloses the game.
Three pieces, all in outward-rounded interval arithmetic, all inside instruments/interval:
What the box then yields, for EVERY (j, H̄) it contains: the density enclosed on each of 256 plot cells and certified above 0.4292; the value function enclosed at 257 points with its mean removed; and the closure ∫u_x enclosed in an interval containing zero (half-width 2.9e-8), which is periodicity, checked rather than assumed.
With b = 0 the paper states u = 0, m = e^V/∫e^V and H̄ = ln ∫e^V. The same code, run on that case, must enclose j at zero and H̄ around the closed form — or the certifier is not to be believed on the case that has no closed form. It does: j ∈ ±1.0e-13, H̄ ∈ [0.235914349, 0.235914368], and ln ∫e^V, enclosed by the same quadrature on e^V, is [0.235914354, 0.235914364] — inside the box. The value function is flat to 1e−9 at every plotted point. ∫e^{sin 2πx} is the modified Bessel value I₀(1); the enclosure of ln I₀(1) here is a by-product, not a claim.
| quantity | A · b = 0 (the control) | B · b = cos² 2πx (the instance) |
|---|---|---|
| current j | ±1.0e-13 | [0.34611351, 0.34611354] |
| ergodic constant H̄ | [0.23591434, 0.23591437] | [0.17116455, 0.17116459] |
| density range | [0.2905, 2.1471] | [0.4291, 2.3164] |
| box half-widths (j · H̄) | 1.0e-13 · 9.0e-9 | 8.7e-9 · 1.6e-8 |
| closed form ln ∫e^V, enclosed | [0.23591435, 0.23591437] — inside | none known (§2.1) |
| what the paper says | u = 0, m = e^V/∫e^V, H̄ = ln ∫e^V — hit | "we are not aware of any closed-form solution" — enclosed |
git clone https://github.com/carlostoledo1891/cert-machine && cd cert-machine node instruments/afg/battery.js # re-derives the record, 19 checks, 6 red controls node instruments/afg/run.js --check # the record, re-derived and compared byte for byte node instruments/interval/tests/test-quadrature.js # the rigorous integral, and its falsifier
No dependencies: the interval library, the transcendental enclosures and the quadrature are plain Node files in the repository. The record is certs/afg-enclosure.json and carries the sha256 of the code that made it.