A first-order mean-field game, enclosed by its current

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:

• The verified inverse. A float Newton step proposes m; the certificate is the sign check sup φ_j(m−δ) < r < inf φ_j(m+δ) evaluated in intervals, which by monotonicity proves exactly one root in the bracket. Over a cell of x and a box of (j, H̄), the density is enclosed by the two corner inverses, because m is increasing in r and in |j|.
• The rigorous integral. The midpoint rule on 2¹⁴ cells with its remainder h³/24 · sup|f″| added as an interval on every cell — the second derivative of the density and of 1/m enclosed from r″, φ′ and φ″ on the cell. A rule that stays green without its remainder is lucky, not rigorous; the battery deletes the remainder and shows the miss.
• The contraction. A two-dimensional Krawczyk operator on (j, H̄): the map F at the candidate by the rigorous rule, its Jacobian over the box by a Riemann enclosure on 2¹¹ cells, and the requirement that the image lands strictly inside the box. Existence and local uniqueness follow in one step; it closed in one round.

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.

• Claimed. Existence of a classical solution with (j, H̄) in the recorded box; local uniqueness there; the density enclosed pointwise and strictly positive; the value function enclosed pointwise and periodic. All of it for every parameter pair in the box, not at a sampled point.
• Assumed, and cited. Global uniqueness. The paper's Lemma 2.3 proves the operator monotone in L²×L², and uniqueness follows by Lasry–Lions. This page proves uniqueness of (j, H̄) in the box and takes the rest from them.
• Not claimed. Any reproduction of their figures (no table exists to reproduce), any first anywhere — the literature gate on this instance (instruments/afg/FINDINGS_LIT.md) finds no validated enclosure of a first-order stationary mean-field game and says "to our knowledge", with its query log as the evidence and one unread paper as the falsifier. This repository's own mfg-cap page holds the first enclosure of a mean-field game; this one is additive by instance: first order, which the sequence-space kernels cannot reach.
• What decides, what only proposes. The float Newton iterate and the approximate inverse are candidates and are trusted for nothing. The dashed curves in Figures 3 and 4 are drawn from floats and dashed for that reason. Everything solid is an interval endpoint.
• The nearest neighbour. Al Abdulaziz, Ashrafyan, Gevorgyan and Gomes (arXiv:2606.19611, June 2026) prove strong convergence of a mirror iteration for regularized stationary games — a convergence theorem, not an enclosure. The two results are of different kinds and are cited as such.

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.

• Noha Almulla, Rita Ferreira, Diogo Gomes, Two Numerical Approaches to Stationary Mean-Field Games, Dynamic Games and Applications 7(4) 657–682 (2017), doi:10.1007/s13235-016-0203-5, arXiv:1511.06576. Equations (1.1), §2.1, §4.2, Figures 7–8, Lemma 2.3.
• Diogo A. Gomes, Levon Nurbekyan, Mariana Prazeres, One-dimensional stationary mean-field games with local coupling, Dynamic Games and Applications 8 (2018), arXiv:1611.08161 — the current formulation.
• Hussain Al Abdulaziz, Yuri Ashrafyan, Yeva Gevorgyan, Diogo Gomes, Bregman-projected mirror methods for regularized stationary mean-field games, arXiv:2606.19611 (2026) — the nearest neighbour.
• R. Krawczyk, Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken, Computing 4 (1969) 187–201 — the operator.