The maximal value function, drawn

Gomes and Üçer study first-order time-dependent mean-field games with local coupling by monotone operators in Banach spaces:

Their Theorem 1.8 is about structure. Fix a density m for which value functions exist. Among all admissible subsolutions of the Hamilton–Jacobi inequality there is a unique maximal one, u*, and the MFG value functions are exactly the subsolutions that equal u* wherever m > 0 and, at t = 0, wherever m₀ > 0. Off the support, a value function is one member of a set. In this machine's grammar that is the CHOSEN standing, and u* is the DECIDED one.

The paper proves this in every dimension, for non-separable Hamiltonians with power growth, and carries no example. This page builds one.

On the circle of length 6 take H = ½p² − m (their Example 2.7 with H₀ = ½p², f(m) = m, g = 0; Assumptions 1⁺ and 2–7A hold). Look for a parabolic bump of density with a self-similar velocity:

The transport equation forces the velocity −u_x = (ṙ/r) x and, with mass one, A = 3/(4r), B = 3/(4r³). The Hamilton–Jacobi equation on the support then forces one ordinary differential equation, r̈ = −3/(2r²): the crowd contracts. Starting at rest with r(0) = 2, the energy integral is ṙ² = 3(2 − r)/(2r), and the substitution r = 2 sin²θ makes everything elementary:

with θ running from π/2 down to π/3, so r(T) = 3/2 and T = √(2/3)(π/3 + √3/2) ≈ 1.5621. What pulls the crowd inward is the terminal cost: u_T = a(T) φ(x), a parabola out to |x| = 9/4 and a C¹ cap beyond it so that u_T is periodic. Off the support the same u = aφ + b is a strict subsolution — on the parabola because A − Bx² < 0 past r, on the cap because φ′ ≤ 2ρ₀ and φ ≥ ρ₀² give A − Bρ₀² < 0. So (m, u) is an MFG solution in the sense of their Definition 1.1, with a vacuum, and u is one member of U(m).

• The pair. On every support cell the HJ residual −u_t + ½u_x² − m and the transport residual m_t − (m u_x)_x are evaluated in intervals and must enclose zero; on every vacuum cell the strict subsolution inequality is decided by a corner bound (the identity A − Bx² is monotone in |x| and in r, so its supremum over a cell sits at a corner and is evaluated there, where the raw interval evaluation would have refused); u(T) = u_T because b(T) is enclosed at zero.
• The maximal one. For continuous bounded m the maximal subsolution is the value of the control problem with running cost ½|ẋ|² + m and terminal cost u_T — the classical identification, assumed and cited. Since m ≥ 0, the free Hopf–Lax value min_y [d(x,y)²/(2(T − t)) + u_T(y)] is a lower bound, computed by a rigorous branch-and-bound over y. The cheapest path proved clear of the crowd is an upper bound: the resting path always is, because the support only shrinks; a surviving minimiser's straight path is, when sixteen interval checks along it stay outside r(s). Where every minimiser is clear the bracket closes and u* = HL exactly.
• The gap. Maximality says u* ≥ u. On every decided cell the upper end of u* must clear the lower end of u, and it does; on 786 cells the lower end of u* clears the upper end of u, which proves the gap positive there. That gap is the space Theorem 1.8 leaves for the other members of U(m).

At each time the shaded band is the support. Inside it the two functions are the same function. Outside it the dotted parabola is u, one admissible value function; the solid bracket is where u* lives. Early on, the bracket is wide far from the crowd: a free path from there has time to dive into the crowd, so the free value is only a lower bound and the resting path only an upper one. Near the horizon the bracket collapses and u* is the Hopf–Lax value.

• Claimed. The explicit pair is an MFG solution with a vacuum, verified cell by cell; the maximal value function is enclosed on every vacuum cell and equals u on the support; the gap is positive where proved.
• Assumed, and cited. That the maximal subsolution of Theorem 1.8 is the control value (the viscosity solution) for this Lipschitz density — classical, and the paper itself lists the general characterisation as open.
• Ours, and said so. The instance. The paper has no worked example; the contracting parabolic bump is the first-order analogue of the parabolic profiles of gas dynamics and is used, not claimed. The literature gate is instruments/maxval/FINDINGS_LIT.md.
• Refused. The 80 cells the moving boundary passes through. A finer grid shrinks them; nothing about them is claimed.

node instruments/maxval/battery.js     # re-derives the record, 18 checks, 5 red controls
node instruments/maxval/run.js --check  # the record, re-derived and compared byte for byte

The record is certs/maxval-cylinder.json: every cell's standing, u, u*, gap and m, plus the closed forms and the code's sha256.

• Diogo Gomes, Melih Üçer, Existence and Structure for First-Order Time-Dependent Mean-Field Games with Local Couplings, arXiv:2606.28378 (2026) — Definitions 1.1 and 1.7, Theorem 1.8, Corollary 1.9, Example 2.7.
• M. Bardi, I. Capuzzo-Dolcetta, Optimal Control and Viscosity Solutions of Hamilton–Jacobi–Bellman Equations, Birkhäuser 1997 — the maximal subsolution as the value function.
• The grammar: design/grammar.js on this site — DECIDED, COMPUTED, CHOSEN, REFUSED, as stroke.