Project
Lean Formalization of QFT
Lean constructions of the objects a later existence proof would need. The entries below are separate pieces of that work.
Entries
-
P(\Phi)_2
Michael Douglas is constructing the Euclidean P(\Phi)_2 measure in Lean 4. The route is Glimm–Jaffe / Nelson: lattice measures for an even polynomial interaction, then continuum limits, aiming at a measure on tempered distributions that satisfies the Osterwalder–Schrader axioms. I contribute to that repository.
Exponential moments only for quartic P
One step in the construction used a Gaussian bound on exponential moments of the interacting lattice field. For a nonnegative source f, the claim was
\int e^{|\varphi(f)|}\,d\mu_P \le 2\exp\Bigl(\tfrac12 \int \varphi(f)^2\,d\mu_P\Bigr).Newman proved a comparison of this shape for quartic site measures. The repository stated the bound for every even interaction polynomial. A one-site sextic is already a counterexample.
Take a single lattice site, mass 1, and a family of even sextics whose wells at -1, 0, and 1 become sharp. The normalized laws converge to
\nu = \frac{\delta_{-1} + 16\delta_0 + \delta_1}{18}.Most of the mass sits at the origin, so the variance is only \mathbb{E}[X^2]=1/9. At source 9 one has \varphi(f)=9X. The proposed bound is
2\exp\bigl(\tfrac12\cdot 81\cdot\mathbb{E}[X^2]\bigr)=2e^{9/2}\approx 180.The exponential moment still sees the outer wells:
\mathbb{E}_\nu e^{9|X|} = \frac{e^9+8}{9} \approx 901.The same reversal shows up at large finite well curvature, so these are actual lattice measures in the project, not just the limit. I restricted the Lean results that used the bound, including the cylinder Osterwalder–Schrader theorems that depend on it, to \deg P = 4.
-
Fermionic path integrals
I’m writing a Lean library for finite fermionic Gaussians. You choose a finite set of Grassmann generators and an alternating quadratic action
Q_A = \sum_{i<j} A_{ij}\,\theta_i\theta_j,and the Gaussian integral is the Pfaffian of A. The rest of the algebra is Berezin integration, Wick pairings, charged fermions through a determinant, and exact elimination of a block of modes. There is no spacetime in the library; a later construction would supply the modes and the action matrix.