cert-machine · certified theorem · re-proved at every build

Two solutions, provably: certified multiplicity for a non-monotone MFG

Where the coupling of a mean-field game turns anti-monotone — agents HERDING instead of avoiding each other — Lasry–Lions uniqueness theory goes silent. This page holds a theorem in that silence: for the quadratic system on the torus with F(m) = c·m at c = −12, two solutions are enclosed in DISJOINT certified balls at the same parameters — a proof that at least two distinct equilibria exist, produced by interval arithmetic and re-proved during the build of this page by the unit's own battery.

tl;dr

The finding. At one parameter set in the anti-monotone regime, two mean-field equilibria are enclosed in disjoint balls — centres 10.787 apart against a combined radius of 4.72e-13 — with both densities certified positive. Disjoint enclosures at identical parameters are a multiplicity theorem, not a numerical observation; and at the bifurcation point itself the proof REFUSES, as it must.
The mechanism. Krawczyk/radii-polynomial contraction in outward-rounded interval arithmetic, checked by three independent witnesses (the HJB pointwise, the Fokker–Planck pointwise, and a Gibbs identity the solver never uses); the constant state's linearization loses invertibility at c* = -9.8696 = −σ²(2π)² — predicted from the symbol, then measured.
Check it. node legacy/research/mfg-cap/tests/test-cap.js from a clone — 17 checks, six falsifiers that must each turn a target red.

the multiplicity

DISJOINT × 2

c = −12: separation 10.787 vs r1+r2 = 4.72e-13 — two certified solutions at one parameter set, densities positive

the bifurcation

c* = -9.8696

−σ²(2π)² predicted from the symbol, then measured: the determinant changes sign across it

at c* itself

REFUSED

no enclosure can exist at the bifurcation — a verifier that certified there would be broken, and the battery checks that it refuses

the monotone control

5.77e-15

worst enclosure radius across five Lasry–Lions parameter sets (worst Z1 0.0644) — the classical regime certifies routinely

falsifiers

6/6 fired

every planted forgery turned its target red this build — including a perturbed candidate that must be refused

battery

17 checks

the unit's own gate, lifted file-level from the published tree and re-run as this page's build gate

§0 · to scale

How far from touching the two enclosures are

Disjointness is what makes this a multiplicity theorem rather than an observation, so it is worth seeing how much room there is. All three quantities below are lengths in the same weighted norm, so they share one axis; it is logarithmic because otherwise two of the three bars would be invisible.

The two certified solutions sit 10.787 apart while their enclosures together span 4.72e-13 — a factor of about 10¹³. Nothing about this proof is marginal: the balls would have to grow by thirteen decades before they touched. The third bar is the loosest enclosure the monotone control produced across five Lasry-Lions parameter sets, for scale — the classical regime certifies just as tightly, which is why the interesting question was never precision but whether TWO solutions exist at all.

§1 · the object

Where uniqueness theory goes silent

For the stationary quadratic MFG on the torus with coupling F(m) = c·m, positive c is crowd-aversion and the Lasry–Lions monotonicity argument gives uniqueness. Negative c is HERDING — agents drawn to density — and the theory makes no claim. That silence is exactly where computer-assisted proof earns its keep: past the symbol's critical value c* = −σ²(2π)², a non-constant branch leaves the constant state, and whether the two coexist as genuine solutions is a question numerics alone can only suggest.

The certificate answers it. Each candidate is wrapped in a contraction argument (Krawczyk / radii polynomial) in outward-rounded interval arithmetic: an explicit ball, exactly one true solution inside it, the ergodic constant enclosed, the density certified positive. Two such balls, at the same parameters, provably disjoint — centres 10.787 apart, radii summing to 4.72e-13 — is a multiplicity theorem about the SYSTEM, not a statement about a solver.

§2 · the discipline

Three witnesses, one refusal, six falsifiers

The battery this page just re-ran checks the solution three independent ways: the HJB equation pointwise on a fine grid, the Fokker–Planck equation pointwise, and the Gibbs identity m = e^{−u/σ}/Z — which the solver never uses, so it cannot be satisfied by construction. The reduced Hopf–Cole equation is compared against the literature's stated form (the sign-flipped variant fails by O(1)), and the certified Z1 bound is required to dominate a direct sampled estimate — the bound is never allowed to be optimistic.

At the bifurcation point the linearization is singular, no contraction can close, and the proof REFUSES — the battery asserts the refusal, because a verifier that certified there would be broken. And every build fires six falsifiers: forged candidates, disabled terms, wrong-parameter validations — each must turn its target red before the page ships. This build: 6 of 6.

§3 · provenance

Where this comes from, and where the original lives

The unit was lifted FILE-LEVEL from the source lab's published tree (the eligibility criterion for everything public here), and this page is a rebuild in this site's own design system — the original interactive artifact, with the same kernel embedded in its bytes, lives in the public repository (research/mfg-cap in the mfg-lab tree, MIT). The mathematics sits in the mean-field-games literature of the KAUST group and the Lasry–Lions/Cirant multiplicity line; the radii-polynomial framework is van den Berg–Lessard, unchanged. The certification layer, and any error in it, is ours.