Make numerical and math claims from models checkable — VERIFIED with an
enclosure, or REFUSED. Formal proof (Lean, AlphaProof) covers discrete logic; bounds, positivity,
existence, stability — where models actually fail — need a numerical certificate. This page is the
live pipeline: candidate in, independent validated numerics out, no LLM in the loop. Below, eight blind
frontier-model instances (one vendor, two tiers — not a cross-vendor panel) face a decidable hard
mean-field-game bound. They disagreed; most got it wrong; none proved it. The certificate settles the
instance and goes red when tampered.
VERIFIED with an enclosure, or REFUSED. Mutation-tested falsifiers must go red on planted defects.
Eight blind frontier runs disagreed on a hard MFG density bound; an independent certificate settles the instance in about two seconds — enclose or refuse. Scope stays narrow: instance, not theorem.
Each row is one blind attempt: a fresh model instance saw only the
equations and parameters above — never the answer, never the certificate — and was asked, analytically, for the
minimum density and whether m ≥ 0.58 holds. Their exact prompts and verbatim outputs are pinned (their structured returns and quotes; the prompt text is not)
(provenance in the footer). The certificate row is the verdict.
| source (blind) | min m est. | m ≥ 0.58 ? | proof? | the model’s own words |
|---|---|---|---|---|
| Claude Opus | 0.573 | says NO | no | “…bound m ≥ 0.58 is marginally violated.” |
| Claude Opus | 0.573 | says NO | no | “A=5 is large enough that higher-order corrections leave this marginal.” |
| Claude Opus | 0.585 | says yes | no | “…holds but only marginally and not provably.” |
| Claude Opus | 0.590 | says yes | no | “…holds — but A=5 exceeds the perturbation radius, so this is an estimate, not a rigorous proof.” |
| Claude Sonnet | 0.561 | unsure | no | “…I would not trust this to 3 significant figures.” |
| Claude Sonnet | 0.520 | says NO | no | “…a minimum density m_min ≈ 0.52 at x=0, below 0.58.” |
| Claude Sonnet | 0.570 | says NO | no | “…so the bound m ≥ 0.58 most likely fails.” |
| Claude Sonnet | 0.550 | says NO | no | “…too large for this to count as a rigorous bound; most likely fails.” |
| ∎ certificate | ≥ 0.5889178 | ENCLOSED YES | enclosure, not a proof | interval arithmetic + radii-polynomial at A=5, N=20; r = 4.3e−13; every falsifier red |
This is not a strawman. The models are careful and reason well: 6 of 8 explicitly flagged that
A=5 is outside the perturbation regime, and one even named the right mechanism — that congestion
“lifts the density trough” above the naive linear estimate of 0.561. Two landed the correct answer. And still:
none could prove it, they disagreed with each other by more than the whole distance to the truth, and the majority
concluded the false thing. The certificate’s value is not catching a dumb error — it is supplying the rigor
no model has and resolving a genuine disagreement.
“For the discounted congestion MFG
u − sigma u″ + (1/2)(u′)^2/sqrt(m) = A cos(2 pi x) + gamma m,
m − sigma m″ − (sqrt(m) u′)′ = 1 at
sigma=0.5, gamma=0.5, A=5, the equilibrium density satisfies min_x m(x) >= 0.5889178, and the solution
exists and is locally unique within the enclosure radius.”
— the claim record’s statement, verbatim
Two qualifiers the claim sentence does not carry, and this page does. (i) Local uniqueness is now enclosed in the full ℓ¹ν ball (even+odd): Φ preserves parity at this instance, so DΦ is block-diagonal; Y₀ is unchanged and one extra Z₁odd bound closes Stage 2.2 (gated; Z₁odd ≈ Z₁even ≈ 0.927 at A=5). (ii) Existence for this system is not ours and, at this instance, is not verbatim inside the theorem that owns it — see “Honest scope” below.
Scope, quoted from the claim record:
“the single certified instance; the surrounding law over gamma is NOT claimed here”
— the claim record’s scope.description, verbatim
The box: A [5, 5] · gamma [0.5, 0.5] · sigma [0.5, 0.5] — governing parameter point; N is the inverted Fourier block size used by the enclosure, not a claim about a truncation of the PDE. The certificate was computed at N = 20. A single point in parameter space. 0.5889178 is a number about that instance, not about the model at large: nothing here is claimed at any other A, or in the continuum limit as a separate theorem. Two things WERE measured outside the box and are reported below rather than omitted — a 130-sample float sweep over A ∈ [0.05, 6.50], and the point at which the enclosure stops closing altogether (A = 5.55). Neither is inside the claim.
The enclosure works in the weighted sequence Banach algebra ℓ¹ν (ν > 1) with an explicit analytic tail on Z₁ beyond the inverted block. That is why the enclosed zero is a real-analytic classical solution of the PDE on the torus — not a Galerkin truncation with leftover projection error. The printed existence radius r = 4.33e−13 is the smallest radius where the radii polynomial closes; the contraction / uniqueness window reaches up to min(rMax, rCap) (rCap = 1e−2 in this family), orders of magnitude larger. Stating only the tiny r as uniqueness understates what the certificate already proves. Full even+odd local uniqueness at that radius is mutation-tested (Stage 2.2: Z₁ = max(Z₁even, Z₁odd)).
| Statement | Status | Evidence, and what it does not reach |
|---|---|---|
| minx m(x) ≥ 0.5889178 at σ=0.5, γ=0.5, A=5, N=20 — the claim | certified | Not asserted — derived by a gate that recomputes the evidence level from the records and refuses to accept a declared one — not what any
status string says. Survived 8 named mechanical attacks along 8 distinct vectors,
each with a passing kill-control. This is not a proof and does not claim the vector set spans the ways this
claim could be false.
the claim record’s attack evidence — eight survivals, each with its own kill-control,
0033, 0035 |
| The radii polynomial closes at this instance: r, Y₀, Z₁, Z₂ and the discriminant | enclosed | r = 4.332607412139519e−13, Y₀ = 3.0067633837811714e−14,
Z₁ = 0.9271316033691069, Z₂ = 63.43867878981078,
disc = 0.005309803223742246. One instance.
the certificate’s bounds |
| The density and the physical reciprocal branch, bounded below over the WHOLE ball | enclosed | min m ≥ 0.5889178299249256, min w ≥ 0.8347598216161033, over the ball — not merely at
the candidate. A lower bound on the value; it says nothing about where in x the minimum sits.
the certificate’s positivity walls |
| Every falsifier the enclosure ships with turns RED | enclosed | 7 falsifiers X1–X7 (outward rounding, perturbed a₀, pointwise witness, dropped 1/m^(a+1), parity, density wall on a wide ball, w>0 branch gate), each required to refuse its own target. the certificate’s falsifier list, every one red |
| The Python verifier and the JavaScript kernel agree bound for bound | enclosed | Agreement 0.00e+00 on every bound. This is a transcription gate, not an independence gate — anything the shared formulation gets wrong identically in both languages passes it. the certificate’s cross-language agreement record; the adversarial adjudication §4 |
| The bound holds across a swept range of A, not only at the claimed point | measured | 130 samples over A ∈ [0.05, 6.50] step 0.05, 0 violations, 0 non-converged, at σ=0.5, γ=0.5, N=20, G=256. Float measurement, not an enclosure. the 130-sample measurement run |
| Where the enclosure stops closing — the refusal boundary | measured | Last closing A = 5.5 (Z₁ = 0.9987220202233071); first refusing
A = 5.55; 20 refusals from 5.55 to 6.5; 1 wall crossing. Reported, not hidden:
the claimed instance sits 0.55 below the wall.
the measurement run’s refusals and observations |
| Full even+odd local uniqueness at r = 4.33e−13 | mutation-tested | PLAN Stage 2.2: Φ preserves parity ⇒ DΦ block-diagonal ⇒ Y₀ unchanged. Odd-block Z₁ enclosed with the same approximate-inverse + analytic-tail structure as the even block (Z₁odd = 0.927131603369091 < 1 at A=5; worst column m₂₁, matching even). Radii polynomial consumes Z₁ = max(Z₁even, Z₁odd). Gated by the congestion validate battery P1b/D1b (dRowOdd vs hybrid odd-residual FD). Stage 2.2 of the congestion enclosure |
| Existence at this instance, inside the theorem that owns existence | outside | Gomes–Mitake Thm 1.1 assumes (A2) V globally bounded; V = A cos 2πx + γm is unbounded in m, so existence at this instance sits outside Theorem 1.1 verbatim. Their uniqueness half does cover it. Not a novelty claim — the authors place unbounded V outside the theorem themselves. arXiv:1407.8267 Thm 1.1 and closing remark, body-read 2026-07-27 |
| Rung 4 — certified | certified | Reached, and this row is kept rather than deleted because how it closed is the point. It was open for a
real reason: prose corrections changed the verifier’s bytes, a certificate is bound to bytes, and the
recorded verifier.sha256 stopped matching — so the ledger gate (check-ledger) derived rung 3 and
this page said rung 3. A stale pin is the gate working, not a formality. The record was then re-frozen
against the new bytes; the recorded hash and the shipped verifier agree
(67822a77… at that re-freeze; 5fd01be3… since
2026-08-05, when the verifier was hardened after a preregistered perturbation run
measured five of its stages silent to the verdict — witnesses now load-bearing,
verdict line carries a full-state digest, the mathematics untouched and re-verified
digit-for-digit before the re-freeze; the run and the fix are on the
errata log) and the ledger gate (check-ledger) derives certified.
This row itself then went stale in the safe direction — it kept saying rung 3 after the re-freeze,
so the page understated its own status until 2026-07-30. Recorded because a page that only publishes the
corrections flattering to it is not publishing corrections.
the certificate’s recorded verifier hash, checked against the file on disk |
| Literature occupancy of the claim | partial | Verdict PARTIAL: existence/uniqueness as bare mathematics is occupied (Gomes–Mitake, hardened by a full body read); only the validated-numerics-enclosure tier came back CLEAR, and that is the load-bearing one. Two bounded sweeps, not an exhaustive review. the claim record’s literature gate |
| “Proved” in the mathematician’s sense | never here | Rung 5 is reachable only by a named human reviewer signing a proof. No agent path exists, and none is asserted anywhere in this file. |
One badge word per meaning, and none of them borrows a rung the claim does not hold.
adversarially-tested eight independent attempts to break the claim survived, each paired with a control proving that same attempt kills a deliberately falsified version ·
certified the ladder’s rung 4, derived by a gate
from the records and never declared ·
enclosed a quantity enclosed by the certificate record —
a property of the record, not a ladder rung ·
measured a float-kernel measurement, not an enclosure ·
unreached a statement no vector in the attack set tests ·
open a leg that is missing ·
never here unreachable by any agent path, on this page or any other.
Read “certificate”, “certifier” and “enclosure” on this page as names for the
object and for the certificate the record — never as the claim’s ladder status, which is the rung word in
the first row and nothing else. Where CONGEST CAP: VERIFIED appears it is quoted stdout from
the downloadable file, reproduced because you can produce it yourself.
The enclosure closes a radii polynomial
p(r) = ½Z₂r² − (1−Z₁)r + Y₀: if it has a root, there is an exact
solution within r of the numerical candidate, locally unique in that ball in the full ℓ¹ν
(even+odd) space — Stage 2.2 closes the odd block with one extra Z₁ bound; Y₀ is unchanged
because the candidate is even — and the density’s minimum over the whole ball is enclosed. Set the three bounds yourself.
The real A=5 values close it; push the contraction
Z₁ past 1 and it refuses — a certificate that cannot go red is fake.
At the real values (Y₀=3.0e−14, Z₁=0.927, Z₂=63.4) the polynomial closes at r=4.3e−13, and a separate positivity wall — also in interval arithmetic, also over the whole ball — encloses min m ≥ 0.5889178 > 0.58 for the A=5, γ=0.5, σ=0.5, N=20 discretisation and for no other. All seven falsifiers (perturb the candidate, drop the reciprocal factor, flip a parity, widen the ball) turn red. The downloadable verifier re-derives every one of these numbers from scratch.
The certificate above is not a picture of the computation — it is the
computation, and you can execute it. Download the single self-contained Python file and run it. It re-derives the
radii-polynomial bounds in outward-rounded
interval arithmetic (math.nextafter), certifies both positivity walls, and refuses every one of seven
tampered variants. Standard library only; no install.
python3 verify_congest.py → it ends in CONGEST CAP: VERIFIED,
printing min m over ball ≥ 0.588918 and seven RED ok falsifier lines. The same kernel runs in
two languages: a cross-language gate (test-crosslang-congest.py) confirms this Python verifier reproduces the
JavaScript source to 0.00e+00 on every bound — an index, parity, or rounding bug on either side would move at
least one number.
The candidates are real, blind, and pinned. The eight rows are verbatim outputs from fresh Claude instances
(model IDs read from the run transcripts’ own API metadata: claude-opus-4-8 for the four Opus rows and claude-sonnet-5 for the four Sonnet rows, 2026-07-23). This is one vendor at two capability tiers, not a cross-vendor panel — read it as such. Each was given only the equations and parameters, with no access to the answer or the
certificate, and asked to reason analytically. Nothing was cherry-picked: every blind attempt is shown, including the two
that reached the right answer. A companion run at weak forcing (A=0.3) is omitted from the scoreboard on
purpose — there the same models solve the problem almost perfectly (~15/16), and showing only the hard case
would be dishonest. The instance was chosen because it is the regime where a good heuristic (perturbation theory) silently
fails, not because models are generally weak.
One instance was not fully blind, and we say so. Seven of the eight made zero tool calls, as instructed. The eighth — the Sonnet row reading “…too large for this to count as a rigorous bound” — also ran a directory listing of the congestion project (find … -type f). It saw filenames only: no file contents, no certificate, no density figure. We disclose it because an undisclosed exception reads as concealment to anyone who obtains the run transcripts, and it is one command away. It also did not help: that instance produced a wrong answer (0.55, “says NO”).
The certifier never uses an LLM. It is interval arithmetic and the radii polynomial, vendored from one single-source library. An LLM checking an LLM is exactly the failure mode this avoids; independence is the whole point.
The existence and uniqueness theory is not ours. Existence and global uniqueness for stationary mean-field
games with congestion and quadratic Hamiltonians are due to Gomes and Mitake, Theorem 1.1 (NoDEA 22
(2015) 1897–1910; arXiv:1407.8267), the uniqueness half proved there after Lions (Collège de France
course, 2007–2011). Uniqueness for their class is theirs, and it covers this coupling — their proof needs
only that V is strictly increasing in m, which γ=0.5 > 0 supplies. Existence at this
instance is a different matter: their hypothesis (A2) requires V globally bounded, and this page’s coupling
V = A cos 2πx + γm is unbounded in m, so existence at this instance sits outside
Theorem 1.1 verbatim — the authors themselves place unbounded V outside the theorem, as an adaptation they
sketch rather than prove. Nothing here is a new existence result and nothing here extends their theorem. What this page
adds is the enclosure — and the enclosure’s own local-uniqueness statement is the full ℓ¹ν
ball (even+odd, Stage 2.2), not a continuum existence theorem.
The novelty is narrow, and it is not the packaging. The interval arithmetic is standard (INTLAB, Arb, the computer-assisted-proof literature); the mean-field game is only the demonstration domain; and the pipeline framing is occupied prior art, ruled so by this project’s own literature gate on 2026‑07‑29 after an earlier pass had claimed it. Independent verification of machine-generated mathematical claims is an active and fast-moving lane (arXiv:2607.05226; arXiv:2606.06136; arXiv:2607.23614; arXiv:2603.15617). Our contribution is not that packaging but the substrate: a radii-polynomial enclosure engine reaching PDE-constrained equilibria that symbolic and exact-rational verifiers do not address, with a verifier that is itself mutation-tested.
The prior art on automation and on released artifacts, named. arXiv:2607.05226 grants certification to machine-proposed candidates by the independent verifier alone, and counts a certificate only when its checker passes in a fresh process. arXiv:2606.06136 ships one artifact carrying certificate, independent verifier and a from-source rebuild route. DualityCert (arXiv:2607.23614) releases verifier, benchmark, protocol and every per-attempt record. arXiv:2603.15617 (HorizonMath) and arXiv:2605.16407 (Proof-Carrying Certificates for LLM Pipelines) occupy the reward-signal and commercial-deliverable framings. Automation, verifier independence, and a released re-executable artifact are prior art, not our claim — and we say so rather than repeat the sentence an earlier draft of this page carried. Two further neighbours bound the substrate question from opposite sides: Colbrook, Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems (arXiv:2606.23821), applies validated numerics to catch an AI overclaim, as a narrated human-decisive case study of two eigenvalue problems; Kim & Pilanci, AI-Assisted Discovery of Convex Relaxations via Dual Agents (arXiv:2606.31182), certifies AI-proposed bounds in rigorous interval arithmetic inside an agent pipeline, on convex-relaxation constants with dual-feasibility certificates. Neither encloses a solution of a coupled nonlinear operator equation; that is the capability boundary, and a boundary is not a priority claim. The closest neighbour by name, Proof-Carrying Numbers (arXiv:2509.06902), is a different layer again — it checks a displayed number against an external reference, not the mathematical truth of a bound from first principles.
The one negative claim on this page, in its attributed form. We are not aware of published work that ships a radii-polynomial enclosure engine as third-party-executable infrastructure for adjudicating machine-generated claims, with a verifier demonstrated to fail on a deliberately broken input. This is a negative claim about a literature; the evidence is a documented search, not a proof. Two limits on it, stated because they are the ones that could sink it. arXiv:2606.08960 (hacker–fixer loops) was seen at search level only, has not been read at source, and may occupy exactly this. And the automation-side sweep that produced the four identifiers above is a single pass over arXiv metadata, with no commercial or product literature searched — a material omission for a question with a commercial edge.
This is a sandbox demonstration, not a published result. The A=5 congestion certificate is genuine and reproducible; the surrounding claims about the field are the ones still being checked.
| what | command (as recorded) |
|---|---|
| the enclosure itself (the downloadable file) | python3 verify_congest.py — the certificate’s own reproduce command |
| the cross-language agreement gate | python3 test-crosslang-congest.py — the Python and JavaScript implementations, compared bound by bound |
| the falsifiers, watched going RED | python3 verify_congest.py — the seven broken variants ship inside it and every one must refuse |
What this page rests on, and what you can check yourself. The evidence behind every number above is a claim record stating the instance and its scope, a certificate recording the enclosure and its reproduce command, two measurement runs, sixteen adversarial attack records (eight independent attempts to break the claim, each paired with a control proving that same attempt could kill a deliberately falsified version), and a falsifier whose breaking patch is watched turning the gate red. A separate literature check, and an independent adjudication of the attack results, are recorded alongside them. Those records are internal, and this page deliberately does not print their identifiers. An identifier a reader cannot follow is a dangling pointer, and on a page whose whole pitch is don’t take our word for it that is worse than saying nothing. What ships instead is the thing that actually settles the question: the verifier. It is one file, standard library only, and it re-derives every bound in front of you in about two seconds — so nothing here needs to be taken on the authority of a record you cannot open.
Every numeral on this page is emitted from an internal record by a generator, never typed by hand: if the generated block and the prose ever disagree, the block is right and the prose is the bug. That machinery is how this page is kept honest internally, and it is deliberately not reproduced here — it is a wall of record identifiers that resolve only inside the tree that produced them, and a public page printing pointers a reader cannot follow is worse than printing nothing. What replaces it for you is stronger, not weaker: the verifier below re-derives every bound in this page’s certificate from scratch, in outward-rounded interval arithmetic, in about two seconds, with no dependencies. You do not have to trust the trace — you can regenerate the result.
eqcert (interval arithmetic, exact rationals, radii-polynomial /
Krawczyk), the same single-source kernel behind the congestion MFG proof
and the Wardrop reproduction. Method transparency is
deliberate: verification discipline — battery-first, every claim with a falsifier, single-source arithmetic — is
the differentiator, not a trade secret.wf_d6a47ecb-274 (A=0.3, 16 probes)
and wf_915f84f1-6d1 (A=5, 8 probes), 2026-07-23. Certificate: A=5, N=20; r=4.33e−13, Z₁=0.927,
min m ≥ 0.5889178, all 7 falsifiers red; Python↔JS cross-language gate exact.