Theorem-First Frameworks and Claim Grammar

What does it mean to say that a quantum field theory exists, has been reconstructed, or is equivalent to another formulation? This chapter makes those claims precise before applying any theorem.

Enter this chapter

Start with the claim-record page and carry one example through the chapter: a cutoff scalar model, a proposed correlator hierarchy, or a comparison of representations. Helpful background. Wightman, Euclidean, Local-Algebraic, Constructive, and Perturbative Frameworks introduces the physical roles of the main frameworks. Limits, Completeness, and Modes of Convergence supplies the topologies and quantifier discipline used in continuum statements. Duality Claims, Dictionaries, Regimes, and Evidence shows why a dictionary between selected observables is weaker than an equivalence of theories.

Topics

1. Theorem-First Claim Records: Objects, Hypotheses, Conclusions, and Status — Turns an informal assertion into a statement with explicit quantifiers and hypotheses.
2. QFT Frameworks, Object Classes, and Typed Maps — Identifies the objects and directional maps used by different formulations.
3. Existence, Construction, Reconstruction, and Continuum Claims — Separates producing an object from recovering one or taking its continuum limit.
4. Equivalence, Uniqueness, and Comparison Notions — Distinguishes unitary equivalence, quasiequivalence, and categorical comparison.
5. Domains, Signatures, Supports, and Regularity — Explains why domains, supports, and regularity are part of the statement.
6. Positivity, Spectrum, Covariance, and Locality Hypotheses — Places each structural condition on its correct mathematical carrier.
7. Counterexamples, Nonconverses, and Hypothesis Stress Tests — Tests implications by changing one decisive assumption.
8. Machine-Checked Theorem Records and Formal-Proof Provenance — Identifies exactly which encoded statement a proof kernel certifies.
9. Source Authority, Dated Status, and Specialist Review — Matches a claim to a dated source that can actually establish it.

How the ideas fit together

A theorem has a source object, hypotheses, and a target conclusion. Comparing two frameworks additionally requires a map between their objects; matching selected observables does not supply its inverse. The table separates these questions for representative cases.

Its reconstruction, functorial, and representation rows use Osterwalder and Schrader 1975, §§ II–V, Brunetti, Fredenhagen, and Verch 2003, Definitions 2.1–2.2, and Araki and Yamagami 1982, Theorem 1.2. The constructive example is developed in Glimm and Jaffe 1987, Chapters 8–12; the formalized free-field example has the scope described by Douglas et al. 2026, §§ 3–4 and Appendix A (PDF).

Representative theorem records

Representative objects, hypotheses, licensed conclusions, and failure boundaries

Object or framework	Domain and regularity	Essential hypotheses	Licensed result and status	Excluded converse	Adversarial check
Cutoff Euclidean φ4 family	Finite lattice spacing and volume; correlation functions regarded as distributions after interpolation	Specified bare-parameter tuning, uniform moment and tightness estimates, a declared order of ultraviolet and infinite-volume limits, and nontriviality control	Existence of the stated subsequential or full continuum Schwinger-function limit in the stated topology; nothing stronger	Stable simulations or convergent low moments do not prove a unique, non-Gaussian, Wightman-reconstructible continuum theory	Reverse the two limits or hold the bare mass fixed and ask which estimate, convergence mode, or nontriviality statement is lost
Osterwalder–Schrader Schwinger hierarchy	A complete sequence of Euclidean distributions with the theorem's regularity and growth control	Euclidean covariance, symmetry, reflection positivity, clustering where required, and the corrected analytic hypotheses	Reconstruction of a cyclic relativistic theory and Wightman functions, with the theorem's unitary-uniqueness statement	Euclidean invariance, pointwise positivity, or a positive two-point function alone does not give reconstruction	Keep the two-point kernel reflection positive but choose an incompatible four-point function; full polynomial positivity then fails
Locally covariant algebraic theory	A functor from globally hyperbolic spacetimes and admissible embeddings to unital algebras and injective morphisms	Functorial covariance, Einstein causality, time-slice dynamics, and any declared state-space conditions	A theory natural under the specified spacetime embeddings, with locality and dynamics in the stated categorical sense	Agreement of one two-point function on one spacetime does not imply natural equivalence to a Wightman, Euclidean, or second algebraic theory	Ask for the missing object assignments, morphism compatibility, natural isomorphism, essential-surjectivity statement, and state data
Constructive P(φ)2 measure	Cutoff and finite-volume Euclidean measures on distributions, followed by controlled removal of both regulators	Stability, uniform bounds, tightness, reflection positivity, clustering, and estimates surviving the chosen limit order	A constructed low-dimensional interacting model after the continuum limit and reconstruction steps actually established	A nonzero covariance or a finite regulated integral does not prove interaction, uniqueness, universality, or a continuum theory	Replace $P$ by a purely quadratic polynomial: the covariance remains nonzero while every higher truncated correlation vanishes
Quasifree representations of a CCR algebra	States on one fixed Weyl algebra over a specified real symplectic space; local restrictions when local comparison is claimed	Comparison of covariance-induced topologies and the relevant Hilbert–Schmidt condition, or the theorem's local Hadamard hypotheses	Unitary equivalence, quasiequivalence, or local quasiequivalence only at the exact strength supplied by the selected criterion	Isomorphic abstract algebras, matching selected moments, or local quasiequivalence does not imply global unitary equivalence	Alter the infrared sector or append a disjoint spectator representation while preserving the selected local two-point data
Smeared Klein–Gordon field and stress tensor	Test functions for the field; products of distributions constrained by wavefront sets; Wick powers on a common invariant domain	Field equation and propagator choice for φ(f); Hadamard singularity, microlocal product criterion, locality, covariance, and renormalization conditions for composites	Well-defined smeared fields and locally covariant renormalized composites, modulo the classified finite renormalization freedom	The notation $\phi(x)$ is not automatically a point operator, and the stress tensor is not unique before the allowed counterterms are fixed	Substitute a delta distribution or multiply two singular kernels whose wavefront covectors sum to zero
Kernel-checked free Euclidean Gaussian field	A pinned Lean environment encoding a Gaussian probability measure on tempered distributions and explicit Euclidean predicates	Definitions faithful to the intended theorem, imported dependency hashes, a named top-level declaration, and a successful replay without unproved placeholders	A machine-checked proof of the exact encoded free-field existence and properties at that source revision	Kernel acceptance does not prove that the definitions model an interacting theory, that omitted physics was formalized, or that later revisions preserve the theorem unchanged	Change a covariance convention or weaken the encoded positivity predicate while leaving theorem names unchanged, then compare the elaborated statement

Structured table data (JSON).

Review the chapter

A sequence of cutoff measures has a convergent two-point function. Has an interacting continuum theory been constructed?

Solution

No. One still needs a limiting full hierarchy or measure in a specified topology, surviving structural conditions, and a non-Gaussianity argument. A nonzero two-point function is also compatible with a free theory.

Where to go next

Continue to Wightman fields and reconstruction to see the claim structure become a concrete quotient-and-completion construction.

References

• Araki, Huzihiro, and Shigeru Yamagami. 1982. “On Quasi-equivalence of Quasifree States of the Canonical Commutation Relations.” Publications of the Research Institute for Mathematical Sciences 18 (2): 283–338. DOI.
• Brunetti, Romeo, Klaus Fredenhagen, and Rainer Verch. 2003. “The Generally Covariant Locality Principle—A New Paradigm for Local Quantum Field Theory.” Communications in Mathematical Physics 237: 31–68. DOI. Open PDF.
• Douglas, Michael R., Sarah Hoback, Anna Mei, and Ron Nissim. 2026. “Formalization of QFT.” arXiv:2603.15770 [hep-th]. Abstract. Open PDF.
• Glimm, James, and Arthur Jaffe. 1987. Quantum Physics: A Functional Integral Point of View. 2nd ed. New York: Springer. DOI.
• Osterwalder, Konrad, and Robert Schrader. 1975. “Axioms for Euclidean Green’s Functions II.” Communications in Mathematical Physics 42: 281–305. DOI. Open PDF.