A published sufficient condition can tell you a mean-field game has exactly one equilibrium — if someone actually checks it, on your instance, in arithmetic that cannot round. This page ships that checker for a class of finite-state mean-field games. It takes a concrete instance and returns one of three verdicts, each earned: CERTIFIED-UNIQUE, with the condition's slack as an exact rational margin — the margin is the certificate; REFUSED, naming the hypothesis that failed — a sufficient condition failing proves nothing, and the verdict says so; or MULTIPLE, only ever over independently verified witnesses — for the instance below, the three published solutions of a two-state game, each checked as an exact identity. The kernels run live in this page, and the falsifier buttons break them in front of you.
Two different mechanisms both end in the sentence “the solution is unique,” and conflating them is the standard error. A Krawczyk or radii-polynomial certificate proves there is exactly one solution inside a ball — it is silent about everything outside, so it can hold on an instance that has three equilibria. This page's object is the other mechanism: instance-level global uniqueness — exactly one solution anywhere in the admissible class — obtained by machine-verifying a published sufficient condition that is a closed-form inequality in the instance's own data. This site ships certificates of both kinds; they are labeled, and this page never uses “certified uniqueness” without the qualifier.
The condition checked here is Theorem 1 of Cecchin, Di Persio & Fraccarolo (arXiv:2607.22537, 2026 — a preprint at the time of writing): a continuous-time mean-field game on a finite state space Σ = {1,…,d}, transition rates αy(t,x) + b(x,μ), quadratic running cost, so the Hamiltonian H(x,μ,p) = Σy≠x[½(py)−² − b(x,μ)py] is non-separable and classical Lasry–Lions monotonicity does not apply directly. Their theorem: under strong monotonicity of the running cost (A1), monotone terminal cost (A2), a product-weighted Lipschitz bound on the interaction (A3), and the key inequality
(A4) Cf > d(d−1) [ 9Lb² + 2‖Δu‖∞Lb ] with ‖Δu‖∞ ≤ 2(T‖f‖∞ + ‖g‖∞) (their Lemma 1),
the solution of the mean-field game system is unique. The theorem is theirs; substituting numbers into it is folklore; the contribution here is the certificate — every constant computed one-sidedly in the direction that can only hurt the verdict, in exact rational arithmetic, with the margin published and a falsifier that has been watched going red.
For the supported instance class — f and g affine in μ with rational matrices, b in the product-square family κ₀ + λ(Πy≠xμ(y))², which contains the paper's own example — the kernel certifies each constant separately:
| constant | direction | how it is certified |
|---|---|---|
| C_f | lower bound | smallest eigenvalue of the symmetric part of f's matrix on the zero-sum subspace — exact Sylvester positive-definiteness tests on the shifted pencil plus rational bisection — then divided by the ℓ¹→ℓ² factor d. Dropping that factor is the false-certify direction, and the page lets you press it below. |
| L_b | exact | λ, symbolically, for the product-square family — the derivation is four lines and sits in the kernel's header. |
| ‖Δu‖∞ | upper bound | Lemma 1 with exact suprema of the affine f and g over the simplex (vertex maxima — exact rationals). |
| margin | signed exactly | Cf − d(d−1)[9Lb² + 2ULb] as one exact rational; its sign decides, its value ships. |
The two instances in the strip above differ in one number — the cost matrix is 600·I in I₊ and 578·I in I₋, with d = 3, T = 1/100, g ≡ 0, and the paper's own interaction b = (Πμ)². The closed-form margins are exactly 2 and exactly −4/75; the certified margins sit just below each, by bisection slack alone. The pair is the point: a checker demonstrated only on instances it certifies has never been seen refusing, and a check that cannot go red proves nothing.
The condition is sufficient, not necessary. When a hypothesis fails, the checker names it — “REFUSED: A4, margin −4/75” — and asserts nothing about the instance's actual number of equilibria: I₋ may well have a unique equilibrium; this page does not know, and says so. The bounds are conservative by construction, so REFUSED can fire on instances that are in fact unique. That is the price of one-sided arithmetic, printed rather than hidden.
The third verdict never comes from the condition failing. It requires two or more distinct equilibria, each independently verified. The instance below is the two-state anti-monotone game of Cecchin, Dai Pra, Fischer & Pelino (arXiv:1810.05492): states {−1,1}, running cost a²/2, terminal cost G(x,m) = −m·x. Their Proposition 2: for horizon T beyond a threshold, the game has exactly three solutions, with closed forms driven by the roots of one cubic. At the rational parameter point T = 9/10, m₀ = 0, the discriminant T(T+4) = (21/10)² is a perfect square and the three terminal means are exactly −5/9, 0, 5/9 — every solution curve is a rational function of time, so this page verifies each one as an algebraic identity: the consistency cubic vanishes at the exact root, both ODEs hold as cross-multiplied polynomial identities over BigInt rationals, both boundary conditions hold, and the three are pairwise distinct. No integration, no intervals, no floats.
Stated plainly, because the alternative would be theft: the multiplicity is their result, published with the complete solution set. This page's verdict adds machine-checking to a known answer — it discovers nothing, and the verdict object carries that sentence in its own citation field. The honest complement is computed in the same battery: the checker of §2, run on this same instance, returns REFUSED naming A1 and A2 — the sufficient condition fails exactly where multiplicity genuinely lives.
The same grammar extends to a second published condition. Gomes and Saúde's monotone numerical methods for finite-state mean-field games (arXiv:1705.00174; Appl. Math. Optim. 83(1), 2021) rest on their Assumption 2: a constant γ > 0 such that the Hamiltonian satisfies θ·(h(z,θ̃)−h(z,θ)) + θ̃·(h(z̃,θ)−h(z̃,θ̃)) ≤ −γ‖θ−θ̃‖² — a hypothesis they describe as essential to the convergence of their methods, and never compute for an instance. For separable Hamiltonians — their own §2.4 potential form h = h̃(z,i) + f(θ,i) — the z-terms cancel inside the condition, which then reads exactly: strong monotonicity of f in the Euclidean norm. So γ̄ is the same certified pencil eigenvalue the (A1) certificate uses — without the ℓ¹ factor, and the batteries pin the two norms' exact factor-d difference so neither certificate can borrow the other's constant. The first certified instance is their own paradigm-shift illustration (f = Iθ): γ̄ = 1 minus bisection slack, live below, and their stationary solution (15) is reproduced exactly along the way — the solution set is theirs, and the underlying model is Besancenot–Dogguy's, per their §2.5. What a certified γ̄ > 0 buys is stated in their paper's own terms: the convergence guarantee of their methods becomes unconditional for the certified instance, and uniqueness is inherited through their Assumptions 1+2 via Gomes–Mohr–Souza — their theorems, cited, never re-proved, and the halves this certificate does not cover (Assumption 1; the z-concavity half) are stated, not smuggled.
The kernels are spliced verbatim from the repository into this page's script — a battery slices the bytes back out, asserts identity with the sources, and re-runs the verdicts from the page's own bytes against the tree. This section needs scripts; everything above is static prose and stands complete without them.
The uniqueness condition (Cecchin–Di Persio–Fraccarolo's, Theorem 1); Assumption 2 and its consequences (Gomes–Saúde's, with the paradigm-shift model Besancenot–Dogguy's); the small-data uniqueness leg of the wider program (Bardi–Fischer's, arXiv:1707.00628); the multiplicity of the witness instance and its complete solution set (Cecchin–Dai Pra–Fischer–Pelino's, Proposition 2); priority over interval methods for game equilibria (Kubica–Woźniak, PPAM 2009 and DMMS 2015, who verify existence and localize equilibria of continuous games); any statement about an instance when the condition merely fails; any status above conjectured, which is what the repository's evidence derives today.
That for the named instances, the named hypotheses of the quoted theorem hold or fail as computed — exact rational arithmetic end to end, every constant one-sided in the hurting direction, margins as printed — and that the three published witness solutions verify exactly and are pairwise distinct. Both batteries re-run in the repository ritual, and both falsifiers have a mutation-verified red: a kernel with the ℓ¹ factor dropped falsely certifies I₋ and the battery catches it; a kernel with the first ODE corrupted rejects the true witnesses and the battery catches that too.
CERTIFIED-UNIQUE here means: the hypotheses of a 2026 preprint theorem hold for this instance, verified exactly. The implication from hypotheses to global uniqueness is the paper's. The reduction of the witness instance to its planar system, likewise. Both are cited, neither is re-proved, and this page inherits their scope entirely.
The condition class is owned: Lasry–Lions monotonicity classically; the non-separable finite-state inequality by Cecchin, Di Persio & Fraccarolo (arXiv:2607.22537); small-data uniqueness by Bardi & Fischer (arXiv:1707.00628) inside the same paper that constructs multiplicity. The witness instances are owned: exactly-three-solutions by Cecchin, Dai Pra, Fischer & Pelino (arXiv:1810.05492); a two-state game with all equilibria identified by Hajek & Livesay (arXiv:1903.05788 — not implemented here, named because it is next). Interval methods for Nash equilibria are owned by the Kubica–Woźniak line (PPAM 2009; DMMS 9(1), 2015 — existence and localization, no uniqueness verdict); and the general set-computation framework of Kreinovich & Kubica (JUCS 16(18), 2010) proves an ε-approximate two-sided enclosure of Nash sets — and, read at source, its own formalism excludes negation, hence cannot express the global-uniqueness predicate at all: the route to a certified global verdict has to go through a sufficient condition, which is what this page does. The monotone-methods framework whose constant §5 certifies is Gomes–Saúde's, resting on Gomes–Mohr–Souza for uniqueness under monotonicity. Where the argument “class-level worst-case equilibrium analysis is dynamically ungrounded” is needed, it is Piliouras, Gemp, Liu & Marris (arXiv:2607.11752) — and the inference from their critique to instance-level certificates is ours, not theirs. What was not located, by a documented search whose queries, fetch log and falsifier are recorded in the unit's literature file: a prior instance-level global-uniqueness checker for mean-field games in certified arithmetic. That absence is a search record, not a proof.