cert-machine · report · the record is re-derived at every build
The empty region, painted by standing
A first-order mean-field game on an interval with an entry at one end and an exit at the other, from Alharbi, Ashrafyan and Gomes (Applied Mathematics & Optimization, 2026). Where the potential is negative the density vanishes: an empty region, and inside it the value function is not unique. This page takes the paper's own explicit solutions and decides them cell by cell: occupied, empty, or refused where the cell holds the free boundary at the budget chosen. The refused cells are drawn as refused. The two value functions are drawn as two members of a set. And the sentence from the paper's abstract, that contact with the exit does not imply exit, is evaluated as an interval, twice.
tl;dr
The finding. On 256 cells, the density of case 1 is decided zero on the runs (0.086, 0.414) and (0.754, 1.000), decided positive and enclosed on the two occupied runs, and refused on 4 cells that hold the exact roots 1/12, 5/12 and 3/4. The refused length is 4/K at every budget from 16 to 1024. Both value functions are enclosed; they differ by 0.91 at x = 0 and meet at x = 1. x = 1 is in the contact set with exit flux exactly zero in case 1 and exactly −j₀ in case 2.
The mechanism. An interval enclosure of the sine on each cell decides the sign of V; the density is V on the positive cells and zero on the negative ones; a cell whose enclosure straddles zero is refused, and a refused cell must contain a root. The value functions are Riemann brackets from the exit. Case 2 inverts the paper's cubic on every cell for every γ in a box, because the paper prints no γ.
Check it.node instruments/aag/battery.js (18 checks, 5 red controls, under a second) re-derives the record and compares it byte for byte.
refused cells
4 of 256
length 0.015625 — each holds one of the three exact roots; at K = 1024 the length is 0.00390625
the empty region
{V < 0}
m = 0 exactly on 2 runs, m = V enclosed on 2 runs
two value functions
u₊ ≠ u₋
u₊(0) ∈ [0.454, 0.466], u₋(0) its negative; Theorem 1.3 gives uniqueness of Du only where m > 0
contact without exit
flux 0
case 1: u(1) = ψ and m(1) = 0, so nobody leaves through the exit they touch
case 2 floor
m ≥ 0.068
for every γ ∈ [-0.5,-0.3] and every x — a positive current keeps the density positive, as the paper says
falsifiers
MUST REFUSE
the float sign rule paints the root cells; a deleted root; a raised exit cost; a shifted cubic bracket; a zero current
§1 · the instance
An entry, an exit, and a place nobody stands
Alharbi, Ashrafyan and Gomes study first-order stationary mean-field games on bounded domains where part of the boundary is an entry, with a prescribed inflow, and part is an exit, with a cost and a relaxed Dirichlet condition: agents may leave, and pay, but nothing forces them to. Their one-dimensional example (§3.2) on (0, 1) is
with V(x) = γ + ½ sin(3π(x + ¼)). With no inflow (j₀ = 0) the current vanishes and at every point either the velocity is zero or the density is: the solution they exhibit is m = V₊, zero wherever V is negative, with the value function u(x) = ±√2 ∫ₓ¹ √(V₋) — two of them. With inflow j₀ = 1/10 the current is −j₀ everywhere, the density is the positive root of a cubic, and it is positive everywhere whatever V does.
However, as our examples show, contact does not necessarily imply that exit occurs.Alharbi, Ashrafyan & Gomes, abstract
Their figures are made with a finite-difference discretisation of the variational problem and Mathematica's FindMinimum, and carry no error bound. γ for the second figure is read from the plot; it is not in the text.
§2 · the vanishing set
Decided where it can be, refused where it cannot
The domain is cut into K cells. On each, an interval enclosure of the sine gives an enclosure of V. If it lies above zero the cell is OCCUPIED and the density is V, enclosed; below zero the cell is EMPTY and the density is exactly zero; straddling zero, the cell is REFUSED: at this budget the arithmetic cannot say. The three roots of V are exact, x = 1/12, 5/12 and 3/4, and the certificate requires every refused cell to contain one and every root to lie in a refused cell. The root 3/4 sits on a cell edge at every power-of-two budget and takes two cells; so the refused count is four at every K and the refused length is 4/K.
The mathematics of a topologically correct sign map from interval arithmetic is thirty years old: Plantinga and Vegter refine until every cell is decided and then draw a clean curve. What is drawn here is the other thing, and it is the point: the cells the budget could not decide, drawn as what they are.
Figure 1 · Case 1 on 256 cells. The occupied runs carry the density tube m = V; the empty runs carry the decided zero line; the hatched bands are the refused cells at the three roots. The free boundary is not located by this figure; it is exact, and the hatch is the width of the budget.
Figure 2 · The budget ladder. The same interval painted at K = 16, 64, 256 and 1024. The refused length is 4/K each time and the decided runs keep their edges to within a cell.
§3 · the value function
Two solutions, both enclosed, neither chosen for you
Where the density vanishes the Hamilton–Jacobi equation only bounds the velocity, ½u_x² ≤ −V, and the paper's Theorem 1.3 proves the gradient of u unique only on the support of m. So there are two value functions, u₊ and u₋, and picking one is a choice the data does not make. In this machine's grammar that is the CHOSEN standing, drawn dotted. Both are enclosed here by a Riemann bracket from the exit, which is rigorous and about 1/K wide, wider than the density's tube and said so. They differ at x = 0 by 0.908 and meet at x = 1, where both are zero.
Figure 3 · The two value functions of case 1, each dotted because it is one member of the solution set, each with its enclosure as fill. On the occupied runs u is flat (u_x = 0); on the empty runs, shaded, the two branches move apart.
§4 · the boundary
Contact without exit, and contact with it
The mixed boundary conditions are four relations, and each is evaluated as an interval from the enclosed solution. In case 1, V(1) < 0 so m(1) = 0: the point x = 1 is in the contact set, u(1) = ψ, and the exit flux is exactly zero. Nobody leaves through the exit they touch. In case 2 the current is −j₀ at every point by the transport equation, so the same contact carries exit flux −j₀: everybody leaves. The paper's sentence is a theorem about these two cases, and here it is a table.
condition of (3.6)
case 1 (j₀ = 0)
standing
case 2 (j₀ = 1/10)
standing
inflow at x = 0: −m(0) u_x(0) = j₀
0 = 0, m(0) ∈ [0.3536, 0.3536]
decided
[0.100, 0.100] identically
exact by the current
relaxed exit at x = 1: u(1) ≤ ψ = 0
u(1) = 0
contact
u(1) = 0
contact
no entry at x = 1: m(1) u_x(1) ≤ 0
m(1) = 0 since V(1) ∈ [-0.354, -0.354]
decided: flux 0
−j₀ = [-0.10, -0.10]
decided: flux < 0
contact product (ψ − u(1)) · m(1) u_x(1) = 0
0 · 0
holds — no exit
0 · (−j₀)
holds — exit
§5 · case 2
A positive current keeps the density positive, for every γ in a box
With inflow the density is the unique positive root of m³ − V m² − j₀²/2 = 0 at every x. The root is enclosed on each cell by a verified bracket (the cubic is increasing past 2V/3, and the positive root lies there), and because the root is increasing in V and V in γ, the two corners of a cell-and-γ box enclose every root inside it. The paper does not print γ; its Figure 2 shows a line near −0.4. So case 2 is certified for every γ in [-0.5,-0.3] at once, and the band in the figure is wide because it holds them all.
Figure 4 · Case 2, j₀ = 1/10: the density enclosed over every cell and every γ in the box, with its certified floor. The band is the price of not knowing γ, and it is paid in the open.
§6 · the honest boundary
What is claimed, and what is not
Claimed. The paper's explicit solutions satisfy its weak-solution conditions (Definition 2.11) and its boundary conditions (3.6) cell by cell, in intervals; the vanishing set is exactly {V < 0} with the three roots exact; the two value functions are enclosed and distinct; case 2 is positive for every γ in the box.
Not claimed. That the free boundary was found — it is exact, and the refusal is a display of budget. That anything was reproduced to a printed digit — the figures carry none and γ is unprinted. That a certified contour is new mathematics — it is not (Plantinga–Vegter 2004); the display of the undecided cells is the contribution, as the target memory ruled before this page was built.
The width you see. The value functions are Riemann brackets, first order in the cell width, because √(V₋) has no bounded second derivative at a root. The density's tube is the sine enclosure itself. The two widths are different and are drawn as they are.
§7 · check it
Under a second on your machine
node instruments/aag/battery.js # re-derives the record, 18 checks, 5 red controls
node instruments/aag/run.js --check # the record, re-derived and compared byte for byte
The record is certs/aag-empty-region.json; it carries the sha256 of the code that made it, every cell's standing, both value-function tubes and the ladder.
references
Sources
AbdulRahman M. Alharbi, Yuri Ashrafyan, Diogo Gomes, A First-Order Mean-Field Game on a Bounded Domain with Mixed Boundary Conditions, Applied Mathematics & Optimization 93, Art. 40 (2026); arXiv:2305.15952v4 — §3.2 Cases 1 and 2, (3.5)–(3.6), Definition 2.11, Theorem 1.3, Figures 1–2.
S. Plantinga, G. Vegter, Isotopic approximation of implicit curves and surfaces, SGP 2004 — the certified sign map, refined until decided; cited as the method this page deliberately stops short of.
The grammar: playground/warrant.js and design/grammar.js on this site — DECIDED, COMPUTED, CHOSEN, REFUSED, as stroke.