Carlos Toledo
wardrop-repro · a verification layer for the multi-population Wardrop program

A convergent flow finds the equilibrium. A certificate encloses it.

The paper — Bakaryan, Aoun, de Lima Ribeiro, Hovakimyan & Gomes, Distributed Hessian–Riemannian flow for multi-population Wardrop equilibrium, AIMS Mathematics 11(5): 15143–15162 (2026), doi:10.3934/math.2026623 — computes each equilibrium with a globally convergent flow and validates it against a benchmark: existence-by-algorithm plus a numerical match. This page reproduces those results independently and adds the complementary thing a stopping rule cannot give: a certificate. Where the costs are affine (S2) it returns the exact rational equilibrium; where they are nonlinear (S3), a Krawczyk enclosure — an explicit box holding exactly one solution, locally unique; where the instance is degenerate (S1), an honest refusal that displays the non-uniqueness S1 admits — its cost is monotone but not strictly, so the paper’s Theorem 4 (uniqueness under strict monotonicity) does not apply and only the totals are pinned. A stopping rule finds where the equilibrium is; the certificate encloses it — there, alone, and positive. S2 reproduces exactly; S1 reproduces to the paper’s integer rounding — 3 of its 15 printed totals differ, two by one unit of rounding and edge (4,7) by two, which is the erratum below — and the interesting story is S3.

Don’t take our word for it — run the proof yourself. MIT‑licensed — keep the notice, otherwise do as you like.

The certified equilibrium, on the network Figures 1–4, live · by scenario

The same 10-node, 15-edge network as the paper’s Figures 1–4, carrying the reproduction's certified equilibrium flow on each edge. Pick a scenario; view either population, or both side by side — the two flows are drawn as parallel lanes so their paths and numbers never overlap. Conservation is recomputed live from the drawn flows, and the Wardrop gap is the machine-zero certificate the battery gates. Teal = cars (population 1, entering node 1); oxblood = trucks (population 2, node 9).

certified Wardrop gap
conservation (live)
edges carrying flow
flow into exits 8,10
Flows are the certified equilibria (batteries test-certify, test-s3fixed), rounded for the labels. Conservation recomputes node balance live from what is drawn — interior nodes net to zero up to the paper's integer rounding. S1's per-population split is non-unique — its cost is monotone but not strictly, so Theorem 4's uniqueness does not apply; the totals are unique, and the split drawn is one certified representative.

The published Table 1, checked live independent · live toggle

The paper prints Scenario-1 flows rounded to the nearest integer (its own note). Rounding a real conservative flow to integers breaks exact conservation by O(1) at interior nodes — so these integers are the display of an equilibrium, not an exact feasible flow. Below: the per-node Kirchhoff imbalance (should be tiny, from rounding), whether any unused edge offers an improving deviation (should be none), and the one genuinely inconsistent row. Toggle edge (4,7) between its printed total 54 and its component sum 52 and watch the potential conflict appear and vanish.

support / equilibrium
worst interior imbalance
(4,7) potential conflict
Total == Flow1+Flow2 rows
Bars are per-node Kirchhoff net (out−in) for the aggregate flow; the source nodes 1 and 9 (+100) and the exits 8, 10 are omitted. Interior bars are the rounding residual — all ±1/±2, never a structural leak. The certificate we are building does not certify these integers; it certifies the unrounded solution the solver produces, of which Table 1 is the rounded shadow. That is why the honest claim is “our total carries a machine-zero certificate,” never “their table is wrong.”

Does the certificate scale? A 20-node preview synthetic · ours · exact

Not a reproduction. Everything above certifies the paper’s published 10-node network. This panel is a synthetic 20-node / 40-edge layered DAG we designed — no published data — to show the same machinery holds on a bigger graph. Two populations enter at node 1 (cars, Q=60) and node 2 (trucks, Q=40); both route to the common exit set {19, 20} — either population may leave through either exit, and at the certified equilibrium each in fact uses both (cars 22.35 / 37.65, trucks 26.84 / 13.16, computed). The cost is affine and strictly monotone (c^r_k = a_k + b_k(j¹+j²) + g_k·j^r, b,g>0), so the equilibrium is unique — and, with integer data, exactly rational.

Kirchhoff residual (exact)
Wardrop gap (exact)
min off-support slack
flow into exits 19, 20
The certificate is exact over BigInt rationals — no float tolerance: per-population Kirchhoff residual identically 0, support tightness identically 0, no off-support shortcut (min slack = 992891025695182033/874617035610237533 > 0 exact; readout shows 1.135), support positivity, and uniqueness both structural (every per-edge cost Hessian PD) and numeric (a perturbed start reseeds the same exact equilibrium). The float Bellman readout sits below the 1e−15 display floor (measured 1.46e−16). Battery: tests/test-scale.js — 23 checks, red-controlled, incl. an OD regression that recomputes the exit set from the conservation data and fails if this prose disagrees.

Don’t take our word for it — run the proof self-contained · Python · stdlib only

The certified equilibria below are not ours to assert. Download the verifier and run it on your machine.

MIT‑licensed — keep the notice, otherwise do as you like. (The page is CC‑BY 4.0; the file is not.)

python3 verify_wardrop.py — no dependencies. It carries the certified equilibria as data (not the solver) and independently checks, in exact rational + interval arithmetic: S1 refuses the non-unique split while certifying the total; S2’s Wardrop gap is exactly 0 (matching Figure 2 and the certified Table 1 (4,7)=1940/37=52); S3 is enclosed by a Krawczyk contraction. Perturb one flow and it prints REFUSED. Cross-checked bit-for-bit against the Node battery.

What the certificate adds, scenario by scenario v0.7 · reproduced + S3 enclosure

scenariopaper's evidencethe certificatestatus
S1 — linear c=j¹+j²HRF ≈ NLP to 1e−11gap < 1e−15; reproduces Table 1 (dev 1.57); REFUSES unique-split point-cert; face dim ≥ 1 (two equilibria + midpoint)mutation-tested
S2 — cars+trucks, affineHRF ≈ NLP to 4e−8gap < 1e−15; EXACT over BigInt + Krawczyk (O7); flows = Fig 2 exactlymutation-tested
S3 — emissions, cubic speed–flowHRF is its own reference (no NLP)gap < 1e−15; reproduces Figure 4 to rounding (length-independent); Krawczyk enclosure on the paper-faithful costmutation-tested
S3 is where the certificate caught something — in this reproduction's own code. Matching Figure 4 forced a confrontation with the fact that the reproduction's cost did not agree with the paper's: it had dropped the 10⁻³ emission factor (making the emission term 1000× too large) and used a truck-weighted congestion flow where §6.3 specifies the plain total j¹+j². With the paper-faithful cost, the standard solver converges cleanly and S3 reproduces Figure 4a to integer rounding — and because the emission term is then a small correction, it does so for any edge lengths, so the exact sₖ are immaterial and no figure needs reading. Every earlier symptom (“the lengths don't match”, “the solver stalls”) was this one bug. A certificate that makes the implementer confront a 1000× discrepancy in their own cost function is doing exactly its job.

What the verification caught including its own mistakes

The real test of a certificate is what it finds — and the most honest answer is that most of it was this reproduction's own error, dragged into the open by the requirement to match the paper's figures exactly.

wherewhatverdict
Our own S3 costthe reproduction dropped the paper's 10⁻³ emission factor and mis-weighted the congestion flow — caught by matching Figure 4our bug, fixed — the certificate found our mistake
Table 1, edge (4,7)components 39+13=52 but the printed total reads 54 — the one row that contradicts itselfpaper typo — our S1 solve gives 52.43→52
Fig 4b truck (a false alarm)the truck labels seemed not to conserve — but under the corrected cost the truck is different, so the read, not the paper, was at faultwithdrawn — a reproducer misread, retracted
All three scenarios reproduce. Of what surfaced, exactly one is the paper's — a rounding typo in Table 1, stated as such. The instructive one was a bug in this reproduction's cost code, and one flag it raised and then had to withdraw. That is the real reassurance a computer-assisted proof gives: it catches the implementer's mistakes, not only the author's — and it is honest enough to retract its own false alarms.

The paper's own benchmarks standard · theirs

The paper's own Tables 2/3/5, transcribed verbatim (docs/PAPER_FACTS.md) and shown for the record only — not re-run, not graded. Each ℓ² and max diff is the distance to that scenario's benchmark: the Uniform NLP for S1, the weighted-potential NLP for S2. S3 has no independent benchmark — Multi-pop HRF is compared only to itself, so its 0/0 is true by construction; the honest content there is the timings and Gauss–Seidel's 4.6e−3 agreement, not an accuracy ranking. Two things worth seeing directly: the Uniform NLP is the fastest method overall — the preprint’s “interior-point >30 min” remark on this same instance did not survive into the published version, and should not be quoted as the paper’s — and projected gradient — competitive on S1 — collapses on S2 (7.6 s, 2e−4) and S3 (150 s, error 1.06).

scenario / methodtime (s)iterℓ² to benchmarkmax diff
S1 · Uniform NLP (benchmark, fastest)0.00053200
S1 · Uniform HRF0.052105903.52e−121.68e−12
S1 · Multi-pop HRF (most accurate iterative)0.071724741.53e−117.29e−12
S1 · Projected gradient0.00862372.54e−71.39e−7
S1 · Gauss–Seidel (new vs arXiv)0.00808216.08e−72.92e−7
S2 · Weighted-potential NLP (benchmark)0.048488300
S2 · Multi-pop HRF0.088645644.13e−82.28e−8
S2 · Projected gradient (slowest, coarsest)7.583965002.07e−48.93e−5
S2 · Gauss–Seidel0.32830232.02e−71.12e−7
S3 · Multi-pop HRF (its own reference — 0/0 by construction)6.90112497500
S3 · Projected gradient (collapses)150.142180001.06124.72e−1
S3 · Gauss–Seidel13.36629004.55e−32.28e−3

Proof-status ledger every claim, by what backs it

Evidence badges name a MECHANISM, never a status this project awards itself. mutation-tested — a headless battery in this repo checks it and is mutation-tested (revert the check and it must go red). standard — an off-the-shelf result, or the paper's own, cited rather than re-derived. open — known and not done, stated plainly so it is never mistaken for done. workaroundtemporary staging while an alternate route is under trial; after any change to that topic the tag falls (dropped, or promoted to mutation-tested / standard). Never a final status. Every mutation-tested row names the file and check that backs it; run node tests/<name>.js to watch it pass, or mutate the target and watch it fail. The two panels above run a subset live. Deliberately absent: the words proved and certified as a status. Both are rungs on this project’s evidence ladder — rung 5 requires a proof document and a named human signature, rung 4 requires a ledger certificate record — and the ledger holds neither for this reproduction: the only two certificate records that exist scope a stationary congestion mean-field game, not a Wardrop network, so no row below would inherit either word. What backs every row is a mutation-tested battery, which is what mutation-tested says and all it says. This badge read gated until 2026-07-29. Same meaning, wrong word: it collided with the site's Open/Gated access tiers and inverted their sense — here it marked the STRONGEST evidence, there it would mark restricted access — and to any reader outside this repository “gated” reads as you cannot see this rather than a battery checks this. This page is public and unrestricted. The verb certify does survive on this page, for the MECHANISM only — the exact rational solve, the Krawczyk enclosure, the honest refusal, and the readout labels that name their output. That is the product; it is not a status.

claimstatuswhat backs it
Published Table 1 support is a valid equilibrium (no improving deviation)mutation-testedtests/test-coords.js (14 checks, mutation-tested), live above
The (4,7) row is internally inconsistent; 52 is the consistent value, 54 a typomutation-testedtests/test-errata.js (18 checks: 4 independent routes + exact rational 1940/37, integer-verified, with a RED control)
Integer flows are non-conservative only by rounding (±1/±2), as the paper disclosesmutation-testedinterior-imbalance check ≤ 2; the paper's own rounding note
VI existence / uniqueness / Nash-equivalence / HRF convergence (Thms 3–6)standardthe paper (Harker–Pang Thm 3.1; strict-monotone uniqueness; product-set Nash; Bregman/Lyapunov) — audited, correct as printed
Krawczyk / verified complementarity / exact rational KKTstandardAlefeld; Kubica–Woźniak; Breiding–Rose–Timme; folklore
S1/S2/S3 reproduced at machine-zero Wardrop gap (<1e−15, float), S1 bound to Table 1 (dev 1.57)mutation-testedkernel/certify.js + tests/test-certify.js (16 checks, 2 falsifiers red)
The (4,7) equilibrium value is 52.43 (→ 52), settled by the machine-zero solve, not the printed 54mutation-testedtest-certify.js C4; test-errata.js R4 (exact 1940/37)
S2 equilibrium flows reproduce the published Figure 2 EXACTLY (car 2a + truck 2b)mutation-testedtest-certify.js C11 (independent solve, max dev 0)
S2 EXACT over BigInt rationals + Krawczyk box; S1 REFUSES unique-split point-cert (split ∈ null(J))mutation-testedO7 (test-wardrop-interval.js) bound green as the authority — test-certify.js C9
S1 equilibrium set has dimension ≥ 1 (convex face: two distinct equilibria + midpoint witness; totals unique, split not)mutation-testedPhase 3 · kernel/s1-face.js + tests/test-s1-face.js; monotone-VI convexity (geometry-approaches D3) — never a unique-split point-certificate
S3 reproduces the published Figure 4 to rounding under the paper-faithful cost, for any edge lengths (length-independent)mutation-testedtests/test-s3fixed.js (6 checks); gap < 1e−15
A certified Krawczyk enclosure of the S3 equilibrium (location + global uniqueness via enclosed strong monotonicity) on the paper-faithful cost — the ground truth Table 5 lacksmutation-testedkernel/s3-enclosure.js + tests/test-s3-enclosure.js + Stage 2.1 test-monotonicity.js (RED falsifiers; a spurious support refused; Y < 2+√5 discharges Thm 4)
The reproduction's OWN S3 cost had two bugs (dropped 10⁻³; wrong congestion flow) — the certificate caught themmutation-testedtest-s3fixed.js E4 (bugS3 re-injects the bugs; buggy-vs-fixed max car dev 6.91, measured); fixed via certify fixS3
A robust S3 solver (continuation + analytic-Jacobian Newton), cross-verified 4 ways, exists as a general toolmutation-testedkernel/s3solve.js (7 checks); NB the earlier “stall” it fixed was the cost bug, not an inherent difficulty
The public mfg-lab S3 module + the O7 Krawczyk S3 certificate carried the same cost bug — found by this reproduction, fixed across all four copiesmutation-testedfixed 2026-07-23 (commit 18ef273); O7 re-closed the S3 Krawczyk box on the corrected cost (max radius 7.32e−13, W2b); the fix is deployed on the live mfg-lab
enclosure-relative accuracy of independent HRF, PG, and block Gauss–Seidel on paper-faithful S3 (declared η; enclosure as ground truth)mutation-testedPhase 2 · kernel/pg-gs-gap.js + tests/test-pg-gs-gap.js — promoted from workaround W-P1-gap (fallen). Table 5 residuals/timings stay standard (theirs)
Exact multi-population Wardrop certificate on a synthetic 20-node / 40-edge DAG (Kirchhoff & gap identically 0 over BigInt; unique; common exit set {19,20})mutation-testedPhase 4 · kernel/scale-net.js certify() + tests/test-scale.js (23 checks, OD regression); panel above carries the certified candidate as data

Where this stands, and what remains

All three scenarios reproduce; S3 is length-independent (nothing here depends on reading a figure) and now carries a certified Krawczyk enclosure — the location-and-local-uniqueness ground truth Table 5 lacks, since there HRF is compared only to itself. The same 10⁻³ cost bug lived in the public mfg-lab S3 module and its O7 Krawczyk certificate; this reproduction found it, and on 2026-07-23 (commit 18ef273) it was fixed across all four copies, O7's S3 Krawczyk box re-closed on the corrected cost (max radius 7.32e−13), and the fix deployed on the live mfg-lab. The former open PG–GS–HRF gap is now mutation-tested as enclosure-relative accuracy of independent HRF, PG, and block Gauss–Seidel under declared η (Phase 2; workaround W-P1-gap has fallen). Independent PG at the lab duel η=0.4 does not reproduce Table 5's S3 collapse; collapse appears at aggressive η. Table 5's printed residuals remain their run, cited standard.

The frontier — scaling the certificate to bigger scenarios prospective · the program

The three scenarios above are a complete reproduction of the published instance, each scenario carrying its own certificate. The standard they establish — exact where the costs are affine, a Krawczyk enclosure where they are nonlinear, an honest refusal where the instance is degenerate — certifies equilibria, not a particular network size or population count, so it carries to larger scenarios unchanged. What such an expansion needs, stated honestly and badged as not-yet-done — a program, not a claim:

expansionstatuswhat it needs — and what stays the same
Larger networks (more nodes / edges) — first specimen: synthetic 20-node previewmutation-testedPhase 4 · panel above + tests/test-scale.js; further size (TNTP / national) stays the programme, not a claim
More populations (P > 2)prospectivethe VI is a Cartesian product (the paper's Theorem 5), and the per-population certificate already carries two — P populations is bookkeeping, not a new argument
Richer cost families (other emission tables, elastic demand)prospectiveaffine cost → exact; smooth nonlinear cost → enclosure; degeneracy → refusal — a new cost family slots into the same three-way standard, S3's cubic speed–flow being the template
enclosure-relative PG–GS–HRF accuracy (emissions case, declared η)mutation-testedPhase 2 closed the former open row; Table 5 timings stay standard
Strict monotonicity of the cost operator (Thm 4 hypothesis) checked in interval / exact arithmeticmutation-testedPLAN Stage 2.1, gated by tests/test-monotonicity.js (in make check): S1 det S = 0 (not strict — refusal of a unique split); S2 det S = 15/16 exactly; S3 Y = sk·(dbase/djeff) enclosed below 2+√5 on jeff∈[0,Q1+Q2] (Yhi ≈ 1.5423 at Fig 3a lengths). Strong monotonicity upgrades the S3 Krawczyk box from local to global uniqueness and discharges the former ASSUMED Thm 4 line. Missing 1e−3 emission factor ⇒ Y ≫ 2+√5 (falsifier RED)
The same standard on other equilibria (stationary MFG, price formation)prospectivethe certificate is formulation-neutral by design — exact / enclosure / refusal is a discipline about equilibria, not about networks; a network VI here is that discipline on one operator among many
The honest content of this section is that the standard is well-defined and portable. One expansion row now carries a first specimen (the synthetic 20-node panel above); the rest remain prospective, open, or (temporarily) workaround. A bigger-scenario program scales the certificate; it does not weaken it. Whatever the size, an equilibrium ships exact, enclosed, or honestly refused — never merely “within tolerance.”

What this reproduction will not claim

Never “their table is wrong.” The one genuine paper slip — Table 1's (4,7) row — is a typesetting artifact, stated generously; the reproduction's own claim is only that its totals carry a machine-zero certificate. The one flag raised against a figure (the Fig 4b truck exits) turned out to be a reproducer misread, and was withdrawn.

The certificate certifies the equilibrium, not the optimum. The paper studies Wardrop I only; the VI is not a potential minimizer except under structure it does not impose. Nothing here describes HRF as “minimizing” in S2/S3.

The method is standard; the reproduction and its self-correction are the substance. Krawczyk, verified complementarity and exact rational solves are off the shelf. What is real here: an independent, proof-carrying reproduction of this non-variational multi-population system — one honest enough to find, and fix, a 1000× error in its own cost code.

Nothing grades the HRF solver. The timings and step counts (Tables 2/3/5) are reproduced for the record only — not re-run, not ranked. HRF finds the equilibrium; the certificate encloses it. Two layers, not two competitors.

No external referee yet. Every claim here has been through independent internal adversarial review — multiple passes that re-derive each result from scratch and try to break it — but all of it is one studio's own scrutiny, not the external referee it has not yet had.

An independent, proof-carrying reproduction of Bakaryan–Aoun–de Lima Ribeiro–Hovakimyan–Gomes, AIMS Mathematics 2026. Every number is regenerated from a headless battery that extracts the solver kernel and prints the sha256 it validated; every check is mutation-tested; the whole page is one file — no libraries, no build step, no network.

Carlos Toledo builds computer-assisted proofs for mean-field games and network equilibria. Where a paper reports a converged iterate, these notes return a certificate — an exact-rational or interval enclosure of the equilibrium, with its location certified and — once strong monotonicity of C is enclosed — its global uniqueness, or an explicit refusal where the instance is degenerate. Certificates over tolerances; a falsifier behind every claim; a green run is evidence precisely because a broken one is built to go red.

For a research group this is a way to validate and stress-test a published result — independently, and in good faith. The same machinery certifies numerical and optimization claims — the kind a frontier system must be able to depend on rather than merely hope for.

Elsewhere in this work. A second enclosed report — a validated-numerics enclosure of a stationary mean-field game with congestion, an instance the scalar reduction cannot reach. And the laboratory, where the Hessian–Riemannian flow of this paper runs live in the page: the equilibrium is solved in the browser and its certificate is recomputed as you move the parameters, including the projected-gradient comparison this reproduction measures.

Carlos Toledo · carlos@carlostoledo.co · on the open-source eqcert certification kernel (MIT) · 2026

Licence. This page — its text, figures, tables and layout — is licensed CC‑BY 4.0: share and adapt it, with credit to Carlos Toledo and an indication of changes. The verifier it carries (verify_wardrop.py) is MIT, not CC‑BY — as is the eqcert kernel it is ported from; the full MIT text and its copyright notice travel inside the downloaded file, so the file is self-sufficient once it leaves this page. The solver that produced the certified candidate is not published and is not licensed here. The reproduced network and Table 1 values remain the work of their authors, cited above. Full terms: technical-reports/LICENSE.md.

Source & the open eqcert standard on GitHub