Computer-assisted proof is a mature field. MFG is a mature field. The intersection looks thin, and this tree is already sitting in it without saying so.
Nothing on this page is claimed, certified, enclosed or proved. No kernel, no certificate, no falsifier, no ledger record, and no literature gate has run on it. It names a direction and what would have to be true. A prospectus that reads like a result is the defect, so this one says so at the top and is not published.
mfg-congest, mfg-cap and ai-verify all enclose in
ℓ¹ν with an explicit analytic tail. With ν > 1 that makes the
enclosed zero a real-analytic solution of the PDE — an existence theorem, not a
numerical result. The congest paper has zero occurrences of Fourier,
ℓ¹, tail or analytic solution. The papers understate themselves,
and the correction is exposition, not mathematics.
MFG is hard because HJB runs backward and Fokker–Planck runs forward, coupled. The entire numerics literature is organised around fighting that — fictitious play, Anderson acceleration, proximal and crossed-monotone schemes, all of which this tree also implements.
The radii-polynomial approach does not have the problem. It treats the
coupled system as one operator F(x) = 0 in a Banach space and encloses a zero. Time
stepping is what makes forward–backward hard; zero-finding in sequence space never
time-steps. The difficulty the field is built around is an artefact of the framing, not of the
equations — and this tree has been exploiting that for months while describing it as
“no discretisation bridge left to build”.
| Requisite | State |
|---|---|
| ℓ¹ν sequence space with analytic tail | eqcert/src/sequence.js — exists |
| Radii polynomial + Krawczyk | eqcert/src/radii.js — exists, with the self-map/contraction gap now fixed |
| An occupancy verdict on CAP×MFG | DOES NOT EXIST. Nakao, Plum, Lessard, van den Berg, Mireles James are the names to clear. This is the whole bet. |
“The enclosure is an existence theorem” holds for SMOOTH mean-field games. It does
not hold everywhere. The argument runs through ℓ¹ν with a geometric tail,
which requires the solution to be analytic — and a state constraint breaks that. In a
heterogeneous-agent economy the borrowing constraint kinks the value function, so V
is not analytic, the tail machinery does not apply at all, and what could be certified is the
discrete equilibrium rather than the continuum one.
Found while writing huggett-rational.html (PATH 12), which is
where the detail sits. Recorded here because a programme claim with an unstated boundary is the
species of overclaim this tree exists to prevent — and because the boundary is genuinely
useful: it says which MFG families the programme covers and which it does not, which is a better
pitch than an unqualified one.
If CAP-for-MFG already exists, this path collapses to
Stage 1 exposition — still the highest-value work in PLAN.md, but a paper about
our own results rather than a programme. That is a survivable outcome and the reason to gate early
rather than late.