{"id":"palomar/PALOMAR-2026-10-27-000014","url":"https://github.com/scottnarmstrong/RegularityStructures/tree/231a68c9a98369b83a47bf307c58f59c19e7f57f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000014-v1.json","repo":"https://github.com/scottnarmstrong/RegularityStructures","tags":["math.PR","math.AP","msc:60H17","msc:60H15","msc:81T08"],"score":0,"title":"Regularity structures and dynamical Phi^4_3","trust":"high","domain":"math.PR","source":"palomar","authors":["Scott Armstrong"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 / Mathlib formalization of the local well-posedness and convergence of the renormalised dynamical Phi^4_3 model on the three-dimensional torus, after Hairer's Theorem 1.15. For smooth initial data, explicit renormalisation constants built from the massive heat kernel, and every exponent eta in (-2/3, -1/2), the solutions of the equation driven by mollified space-time white noise converge in probability in the Hölder–Besov space C^eta up to the maximal existence time of the limit, and the limit does not depend on the mollifier. A standalone library proves the general theory used: the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"A theory of regularity structures","identifier":"","relationship":"formalizes"},{"title":"A semigroup approach to the reconstruction theorem and the multilevel Schauder estimate","identifier":"","relationship":"formalizes"},{"title":"The BPHZ theorem for regularity structures via the spectral gap inequality","identifier":"","relationship":"adapts"},{"title":"Renormalised dynamical Phi^4_3 on the three-torus: the statement formalised in Lean","identifier":"","relationship":"formalizes"}]}