The Critical 2D KPZ Process
A Lean 4 formalization of "The Critical 2D KPZ Process" by Berger, Caravenna, Clark, Dunlap, Gu, Liu, Nakajima, Sun, Tsai, Xie and Zygouras (arXiv:2610.31614, version 1), together with selected inputs and adaptations in the form these proofs need. For directed polymers on Z^2 in a Gaussian environment at critical disorder, it proves the existence of a critical 2D stochastic heat flow, defined as the joint limit in law of the rescaled partition functions (Theorem A). The centred log-partition function converges in law, in the local negative Sobolev spaces H^{-a}_loc and jointly in finitely…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-28-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-28-000014/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-28-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'