Pick a rectangle of mean-field-game parameters. This decides it: two solutions, one solution, or honestly undecided — and when it says two, it hands you both, each inside a ball with a radius, valid for EVERY parameter in the rectangle. 19,800 cells of the coupling–potential plane are decided below; 11,330 of them carry a proof that uniqueness fails there. The same certifier runs in this page, ships beside it as one dependency-free file, and is in the repository.
Published, not peer-reviewed, not independently rerun. The radii-polynomial machinery is van den Berg–Lessard; the uniform-over-a-rectangle variant, the refutation mode and the partition are this lab’s.
Give it a rectangle of parameters. It solves for both branches, wraps each in a contraction argument over the whole rectangle, and answers. Nothing is uploaded — the certifier below is the repository’s own code, assembled from the same files the map was made with, running in this tab.
Runs in this tab. Nothing is uploaded, nothing is logged; the certifier is the repository's own code, assembled from legacy/core/interval/interval.js, legacy/core/mfg/mfg1d.js, labs/mfg/box.js. A cell takes about a tenth of a second.
Every cell below was decided by the certifier in §1, over its own rectangle. A grid of point results would prove nothing between its points; this is a partition, so the plum region is a set of positive measure on which uniqueness provably fails. Cells that refused were quartered and retried — which is why the resolution sharpens exactly along the two curves the theory names.
Read the seam. The constant state loses invertibility exactly at c*, so cells straddling it refuse — that vertical scar is not a rendering artefact and not a limitation of the solver: it is the theorem’s own hypothesis failing, drawn to scale. To its left the herding branch has been born and the multiplicity region opens; to its right the aligned branch is alone in this family, and the honest verdict is that we enclose it and cannot say it is the only one until c reaches 0 and the classical theorem takes over.
For one parameter triple, the standard argument is Newton–Kantorovich in radii-polynomial form: build an approximate inverse A of the linearisation at a numerical candidate x̄, bound Y0 = ‖AΦ(x̄)‖, Z1 = ‖I − ADΦ(x̄)‖ and the Lipschitz constant Z2, and close ½Z2r² − (1−Z1)r + Y0 < 0. Then an exact solution lies within r of x̄ and is the only one there. That is the lifted kernel, unchanged.
Over a whole rectangle two things go wrong, and both are visible in the code. First, A must be ONE fixed operator or “I − ADΦ” is not an operator at all — so A is built at the cell midpoint, and the tail of I − ADΦ then carries a term 1 − σ/σ₀ that does not decay in the mode index. That is the honest price of a wide σ box, and it is charged explicitly.
Second, and worse: with a FIXED candidate, Y0 grows linearly in the cell width, and the discriminant condition then admits only cells narrower than 0.004 in c on the herding branch — a hairline, not a map. So the candidate travels: the tangent ẋ solving DΦ ẋ = −∂ₛΦ is computed from the Jacobian already factored for A, and the bound becomes a mean-value form whose first-order term vanishes by construction. Y0 drops to second order in the width, and cells 15.6× wider close — 0.0625 in c. Falsifier X2 measures both thresholds on the same ladder by switching the predictor off, so that ratio is a measurement of this build, not a claim about one. The map agrees with it: not one cell of the sweep’s starting width 0.125 certifies multiplicity anywhere, while 2,514 close at 0.0625 and 8,816 close at 0.03125.
Two such certificates over the same cell, with a separation bounded below by more than r₁ + r₂, prove that the cell holds at least two solutions everywhere on it. In the worst cell of the whole map that separation clears the combined radii by a factor of 290; the enclosures are never nearly touching.
The claim is a statement about every point of a rectangle, so battery check C1 re-solves the system at all four CORNERS of a certified cell and measures the distance from each corner solution to the predicted centre. The certificate says that distance must be below r. On the cell it tests, this build measured r = 2.454e-4 against a worst corner distance of 7.029e-5. A uniform claim that failed at a corner would be caught by arithmetic a referee can repeat.
A solver gives you a residual near zero and asks you to believe. This lab will also decide the NEGATIVE, which no solver can: paste a claimed equilibrium and the accuracy you claim for it, and if a single equation’s residual exceeds what the whole ball of that radius could move it, then no exact solution lies that close — whatever the rest of the vector does.
The witness is that one equation, its enclosed residual, and its row bound — three numbers, checkable by hand. A residual near zero is evidence; a residual provably too large is a proof. And the instrument refuses to over-claim in the other direction: hand it a true equilibrium and it returns REFUSED, not a certificate (battery R2). The “refute a candidate” button in §1 loads a worked example, and this build measured its refutation: equation F_1 carries |Φ| ≥ 1.572e-1 while the whole ball of radius δ = 10⁻³ could move it by at most 1.497e-3.
The map is evidence that the tool works at scale. The tool is the point.
node mfg-certify.js '{"sigma":0.5,"c":[-16.03,-15.97],"A":[0.288,0.313]}'
-> MULTIPLE — two exact solutions for every parameter in the cell
git clone https://github.com/carlostoledo1891/cert-machine
node labs/mfg/battery.js # 9 checks, 6 falsifiers
node labs/mfg/regime.js # rebuild the whole map
The browser certifier is not a re-implementation. It is ASSEMBLED at build time from legacy/core/interval/interval.js, legacy/core/mfg/mfg1d.js, labs/mfg/box.js — nothing retyped — and then executed against the Node path and required to give the same verdicts and the same witnesses, or this page does not build. A rule defined twice will diverge; the only defence is a check that fires when it does.
The observatory is the front door, not the whole lab. Each page below is a separate certified result in mean-field games and traffic equilibrium, and each one re-proves its own claims during its own build — nothing on any of them is remembered from a previous run.
NEEDS-DATA is the sharpest verdict a machine can give, and here it is called UNDECIDED. It is a measurement of where this argument stops, not a shrug — and 6,470 of the 8,086 undecided cells still contain a certified enclosure, which means an exact solution is proved to exist there and only its loneliness is open.
| cells | the reason, as the certifier stated it |
|---|---|
| 5470 | only one solution found at the cell midpoint — a second branch is not excluded, it is not exhibited |
| 1127 | aligned branch: discriminant <= 0 — no radius closes the contraction over the box |
| 999 | herding branch: discriminant <= 0 — no radius closes the contraction over the box |
| 489 | aligned branch: Z1 >= 1 over the box — the midpoint inverse does not control the whole cell |
| 1 | herding branch: contraction factor Z1 + Z2 r >= 1 at the smallest admissible radius — T is a self-map but not a contraction |
Three of these are worth reading as physics rather than as failure. “Z1 ≥ 1 over the box” is the cell straddling a singular linearisation — the bifurcation seam. “Density positivity not certified” is the herding density pressing toward zero as the potential deepens, and m > 0 is a hypothesis of the model, so it must be proved and cannot be waved through. “Only one solution found” is the region above the fold where the two branches have collided and annihilated: we exhibit one solution and decline to pretend we know it is alone.
The model and the solver are the KAUST mean-field-games line and the Lasry–Lions/Cirant multiplicity literature; the radii-polynomial framework is van den Berg–Lessard, unchanged. The kernels under <span class="m">legacy/core/</span> were lifted file-level from the published mfg-lab tree, are recorded with their sha256 in <span class="m">PROVENANCE.json</span>, and are never edited here — <span class="m">labs/mfg/box.js</span> is a second implementation of the same argument, which is exactly why the battery demands bit-for-bit agreement with them at zero cell width before this page is allowed to build. The certification layer, and any error in it, is ours.
This lab is not a platform and is not looking for users in general. It is looking for ONE claim at a time. If you work on mean-field games and there is a statement your group keeps having to defend by hand — a uniqueness regime, a numerical equilibrium, a bound someone doubts — send it. If it is decidable, it gets decided here, with the witness, and the answer is yours whether or not it is the one you wanted.
The instruments next door: certified multiplicity at a point, the result this map generalises; a congestion MFG enclosed, whose Hamiltonian admits no Hopf–Cole reduction; Wardrop equilibria reproduced, enclosed and refused; and the methods note.