To our knowledge the first validated-numerics enclosure of an equilibrium for a mean-field game with congestion: from a numerical candidate, an EXACT solution within an explicit radius, locally unique in the full sequence-space ball, with strictly positive density — every inequality in outward-rounded interval arithmetic. The proof travels inside the page: its stdlib-Python verifier was extracted from the published bytes and re-run during this build, and this report refuses to render unless it says VERIFIED.
Every radius where this curve sits below zero is a radius at which the operator is a contraction, so an exact solution exists within it and is the only one there. The curve is drawn from the three bounds the verifier printed during this build — nothing here is fitted or sketched.
The system is the discounted Gomes–Mitake congestion mean-field game on the torus: a Hamilton–Jacobi–Bellman equation coupled to a Fokker–Planck equation, with congestion cost ½(u′)²/m1/2 — the crowd slows you down where it is dense. An earlier certificate in this lineage enclosed a QUADRATIC-Hamiltonian game, which Hopf–Cole-reduces to a Gross–Pitaevskii ground state — a referee can call that "GP in disguise". The congestion game has no such reduction; enclosing it certifies genuinely coupled mean-field structure. The half-integer power is handled by adjoining s = m1/2 and w = m−1/2 through polynomial constraints (s∗s = m, s∗w = 1), so the whole certificate rests on a uniform positive density bound — which is itself certified, not assumed.
The enclosure is NOT a finite truncation with unquantified projection error. Unknowns live in the weighted sequence Banach algebra ℓ¹ν with ν = 1.05 > 1: the defect bound Y₀ is exact by band-limitation, the contraction bound Z₁ carries a closed-form analytic tail over the infinitely many modes beyond the inverted block, and the geometric weight decay forces the enclosed zero to be a REAL-ANALYTIC function — a classical solution of the PDE, not a Galerkin approximation.
Where p dips strictly below zero, the Newton-like map is a contraction on the ball of radius r and has EXACTLY ONE fixed point there — an exact solution, with existence and local uniqueness in the same breath. The verdict is gated on the whole argument, never on a small residual: a tiny defect Y₀ suggests a solution is near and proves nothing; what proves it is Z₁ < 1 together with a radius where p is strictly negative. Local uniqueness holds in the FULL even ⊕ odd ball (the operator is parity block-diagonal at this instance; one extra odd-block bound closes with Z₁ = max(Z₁ᵉ, Z₁ᵒ) = 0.5268), and the admissible uniqueness window extends twelve orders of magnitude beyond the existence radius.
Two failure modes are honest outcomes, not bugs: Z₁ ≥ 1 (the approximate inverse is not one) and a non-positive discriminant (the defect is too large). The instrument refuses rather than guesses — the same contract every certifier in this machine signs.
The proof closes in the moderate regime and REFUSES as the density concentrates: as the crowd piles up, the certificate's contraction bound crosses 1 and the instrument declines to certify. Where it refuses is reported as data, not hidden — the full refusal frontier over the (σ, a) parameter plane is named future work, and nothing outside the certified ball is claimed. A validated-numerics result that cannot show you where it stops working is not showing you where it works, either.
The published page (byte-preserved in the repository, exactly as sent to its readers) embeds its complete verifier — plain Python, standard library only, MIT — as a download. This build extracted those bytes, hashed them (7c5356222d6289be…), ran the verifier, and required VERIFIED plus the exact radius, contraction and density values above; any drift refuses the page. You can do the same: download the extracted verifier and run python3 verify_congest.py — about four seconds, and its planted falsifiers must refuse before it exits green.