Theorem-First Frameworks and Claim Grammar

A mathematical-QFT assertion becomes determinate only after its objects, domains, quantifiers, hypotheses, implication direction, conclusion, and source version are fixed. This chapter develops a common language for doing that work across Wightman, Euclidean, algebraic, constructive, perturbative, and machine-formalized settings. Its central lesson is deliberately strict: a calculation can support a claim, a construction can produce an object, and a theorem can license an implication, but none of those statements may silently be strengthened into existence, uniqueness, equivalence, or a converse.

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.

Enter this chapter

The working unit is not a slogan such as “the model exists” or “the formulations are equivalent.” It is a typed implication

$$\bigl(\mathcal O,\mathcal D,\mathcal Q,\mathcal H;\mathcal S_v\bigr) \quad\Longrightarrow_{\mathcal P}\quad \bigl(\mathcal C,\mathcal U,\mathcal N\bigr),$$

where $\mathcal O$ names the objects and maps, $\mathcal D$ their domains and regularity, $\mathcal Q$ the quantifier and limit order, $\mathcal H$ the hypotheses, and $\mathcal S_v$ the source at a specified version. The proof or construction $\mathcal P$ licenses a conclusion $\mathcal C$ with a stated uniqueness strength $\mathcal U$ and an explicit nonconverse boundary $\mathcal N$. The notation is only a mnemonic; the mathematical content lies in spelling out every entry.

Throughout this volume, Lorentzian formulas use metric signature $(+---)$ and Euclidean quadratic forms are positive. Fields are distributions until smearing and domain control make an operator expression meaningful. A support statement always belongs to a named Fourier convention, a positivity condition belongs to a named carrier, and a limit belongs to a named topology. These are not cosmetic details: changing any one can change whether the proposed theorem is even well-formed.

There are two complementary ways to enter the material.

1. Start from a claim. Identify the primitive object, replace every ambiguous verb by a precise construction or implication, expose the quantifier order, and determine the strongest conclusion actually proved.
2. Start from a comparison. Name the source and target object classes, type the proposed map, check its hypotheses and choice dependence, and test faithfulness, fullness, essential surjectivity, or the weaker property that is genuinely available.
3. Start from a failure. Remove one hypothesis at a time, find the first unavailable step, and retain whatever weaker conclusion survives. A theorem whose hypotheses fail has not been contradicted; it has ceased to apply.

The resulting dependency chain is

$$\text{objects and maps} \longrightarrow \text{domains and quantifiers} \longrightarrow \text{hypotheses} \longrightarrow \text{proof or construction} \longrightarrow \text{licensed conclusion}.$$

At every arrow, a failure test asks whether the preceding data are sufficient. Source version and date qualify the entire chain, not merely its last sentence.

The dependency map applies this sequence separately to each candidate object; the listed examples are parallel cases, not ingredients in one theorem. Follow a row from carrier to conclusion, then inspect the source and nonconverse attached to the last step.

For each candidate separately, a valid claim fixes the carrier and limit order, discharges the hypotheses, applies a named directional result, and states the conclusion’s ceiling and source version. The lower branch is a genuine kernel-checked free-field result at the pinned revision, but it licenses only the encoded Gaussian Osterwalder–Schrader predicates. The diagram is schematic and not to scale. Structured description and source data (JSON)

Representative theorem records

The comparison below is intentionally heterogeneous. Its purpose is to show that the same questions can be asked of a cutoff family, a reconstruction theorem, a functorial theory, a representation comparison, a distributional composite, or a formal proof. The “licensed result” column gives the ceiling, not a prediction about what ought to be true.

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) preserves the same caption, headers, rows, and reading order.

The reconstruction row uses the corrected Osterwalder–Schrader hypotheses Osterwalder and Schrader 1975, §§ II–V, pp. 283–297. The functorial row follows the locally covariant formulation Brunetti, Fredenhagen, and Verch 2003, Definitions 2.1–2.2 and Axioms 1–3, pp. 38–41. For quasifree CCR states, topology and Hilbert–Schmidt conditions are theorem hypotheses, not optional diagnostics Araki and Yamagami 1982, Theorem 1.2, pp. 287–288. The final row refers to the formalized free Gaussian field described by Douglas et al. 2026, §§ 3–4 and Appendix A, pp. 10–15, 25–26.

The failure map performs the complementary test: it preserves the proposed chain until one exact object class, domain, hypothesis, proof step, or implication direction is changed.

Each dashed branch changes one decisive input. Shared two-point data do not establish framework equivalence; a plane wave, coincident product, or swapped limit can leave the theorem’s domain; ordinary positivity does not replace reflection positivity of the full hierarchy; a successful calculation or build does not prove an unencoded theorem; and local quasiequivalence does not imply global unitary equivalence. The diagram is schematic and not to scale. Structured description and source data (JSON)

Reading sequence

The pages form one argument. Each should also be usable independently once its background note has been satisfied.

1. Theorem-First Claim Records: Objects, Hypotheses, Conclusions, and Status turns an assertion into a complete record and applies the method to a regulated $\phi^4$ family.
2. QFT Frameworks, Object Classes, and Typed Maps distinguishes the primitive objects and directional maps of the Wightman, Euclidean, algebraic, constructive, perturbative, and factorization-algebraic settings.
3. Existence, Construction, Reconstruction, and Continuum-Limit Claims separates six often-confused statements and tracks a constructive $P(\phi)_2$ model through its actual implication chain.
4. Equivalence, Uniqueness, and Comparison Notions orders unitary equivalence, quasiequivalence, local quasiequivalence, categorical equivalence, and weaker comparison properties without inventing converses.
5. Domains, Signatures, Supports, and Regularity shows how test-function spaces, operator domains, Fourier support, wavefront sets, signatures, and renormalization freedom enter theorem statements.
6. Positivity, Spectrum, Covariance, and Locality Hypotheses identifies which carrier each structural condition acts on and why no one condition supplies the others.
7. Counterexamples, Nonconverses, and Hypothesis Stress Tests constructs countermodels that remove exactly one proposed implication while preserving as much neighboring structure as possible.
8. Machine-Checked Theorem Records and Formal-Proof Provenance explains what a proof kernel certifies and gives a reproducible record for a formalized free Gaussian field.
9. Source Authority, Dated Status, and Specialist Review matches each claim to the source capable of supporting it and builds a dated packet for a three-dimensional Yang–Mills–Higgs scaling theorem.

A reusable claim check

Before accepting a mathematical-QFT statement, answer these questions in order.

• What is quantified? Name the model parameters, test functions, regions, spacetimes, states, representations, regulators, subsequences, and source versions. Check whether “for every,” “there exists,” and “after passing to a subsequence” appear in the right order.
• Where does the expression live? State the test-function space, topology, operator domain, category, signature, Fourier convention, support condition, and regularity class needed to make the formula meaningful.
• What is assumed rather than derived? Separate positivity, spectrum, covariance, locality, clustering, time-slice, nuclearity, microlocal, and uniform-estimate hypotheses. Similar physical motivation does not make them logically interchangeable.
• Which verb is licensed? Distinguish define, construct, reconstruct, converge, classify, compare, approximate, compute, and conjecture. Attach the conclusion to the exact proof or construction that supplies it.
• How unique is the output? Say whether uniqueness is literal, up to unitary isomorphism, up to natural equivalence, modulo counterterms, within a phase, or not known.
• Which direction fails? State the converse separately and test it with a concrete altered object. A useful counterexample preserves all irrelevant assumptions so the missing step is visible.
• Which source fixes the wording? Use the primary theorem and any correction for the statement, a primary construction for existence, the formal repository and dependency snapshot for a machine proof, and a dated specialist synthesis only for genuinely evolving status.

A passed numerical check, symbolic identity, exact free-field example, or kernel-checked lemma is an independent check of the encoded instance. It is not a proof of a general statement whose quantifiers and hypotheses were never encoded.

Two complete routes through the method

For a continuum claim, begin with the regulated object and write every limit explicitly. Identify the estimates uniform in each removed regulator, the topology in which compactness or convergence is obtained, and the property that distinguishes the limit from a Gaussian or zero theory. Only then ask whether the limiting Euclidean hierarchy meets the reconstruction hypotheses. Constructive field theory succeeds by proving this chain, not by renaming a regulated integral; the standard low-dimensional examples are developed systematically in Glimm and Jaffe 1987, Chapters 8–12.

For a current theorem claim, freeze the exact version before interpreting it. The three-dimensional Yang–Mills–Higgs example later in the chapter records the lattice variables, unitary-gauge projection, coupled parameter limit, convergence mode, and Proca-field output. The theorem does not become a result about four-dimensional pure Yang–Mills merely because both theories contain gauge fields. This boundary follows directly from the proved model and hypotheses in Chatterjee 2026, Theorem 3.2 and the following remarks, manuscript pp. 12–13.

What completion looks like

After this chapter, a reader should be able to rewrite an informal assertion as a typed implication, find the first missing domain or hypothesis, distinguish a construction from a reconstruction, and state the exact uniqueness strength. The reader should also be able to reject a false converse without overstating the counterexample, and to separate a verified computation or formal proof from unencoded mathematical and physical claims.

The practical standard is simple: another reader should be able to reconstruct the claim’s logical form, repeat its independent check, locate the exact supporting theorem, and identify the first change that would make the conclusion unavailable.

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.
• Chatterjee, Sourav. 2026. “A Scaling Limit of SU(2) Lattice Yang–Mills–Higgs Theory.” Probability and Mathematical Physics 7: 339–381. 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.