How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Cook limits, massive wavepackets and scattering obligations
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Areas of Elementary Plane Figures
- Banach Valued Integration and the Radon Nikodym Property
- Banach-Space Differential Calculus and Banach Manifolds
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Convergence: Nets and Filters
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Darboux, L'Hôpital, and Taylor's Theorem
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces Adjoint Operators and Annihilators
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Exterior Powers, Orientation and Hodge Duality
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Probability and the Probabilistic Method
- Foundations of the Real Numbers for Analysis
- Fourier Transform Convolution and Approximate Identities
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fubini and Change of Variables
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Improper Integrals
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Manifolds with Boundary Collars and Orientations
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Orthonormal Bases, Parseval and Fourier Series
- Outer Measure and the Caratheodory Extension Theorem
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Positive-energy tube analyticity and discrete-symmetry proof interfaces
- Power Series and Real-Analytic Functions
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Qm Math Composites
- Radon Measures and the Riesz Markov Kakutani Theorem
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Scalar future mass-shell measure and test restriction
- Schwartz Space and the Plancherel Theorem
- Schwartz/distribution spaces and Hilbert Fock conventions
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Spacetime Primitives
- Spectral Measures and Borel Functional Calculus
- Strongly Continuous Semigroups and Hille Yosida
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tempered Distributions and the Fourier Transform
- Tensor Fields Exterior Algebra and Differential Forms
- Tensor Products of Modules
- Tensor test algebra and positive tempered moment data
- The Analytic Hahn Banach Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Inverse and Implicit Function Theorems
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Unital star algebra and positive normalized state
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
Massive scattering packets and Cook approximant contract
Definition
Assume Countable Choice. Use the positive-energy joint spectral input: a nonzero complex Hilbert space , a strongly continuous translation representation , a projection-valued measure on with and , and an invariant unit cyclic vacuum for a specified unital complex -subalgebra . By the unital star-algebra definition listed below, a unital complex -algebra has a complex-bilinear associative product, a specified unit, and a conjugate-linear involution reversing products, squaring to the identity, and fixing the unit; inherits these operations and contains . Cyclicity means . The pairing is . Use the shell coordinates and signature of the scalar future mass shell definition: for and , and . Here is the positive inverse-length mathematical shell parameter called in that supplier; it is not identified with a measured rest mass. The coordinates have length units, and have inverse-length units, and is dimensionless.
is the positive mass shell; it is closed and hence Borel. Its equivalent parameterization is . It is an isolated massive shell input when and some satisfies The corresponding one-particle space in this contract is the closed subspace . This is an adopted spectral hypothesis and subspace designation; the definition does not infer particle stability from a formal two-point-function pole.
A translation-covariant local net is an assignment of unital -subalgebras of to bounded open , with , such that implies , , and for every when the regions are spacelike separated. Spacelike separation means for every . An operator is local if it belongs to for some bounded open . A bounded operator is norm-almost-local if, for every integer , there is a constant and operators for all , where , such that . The domain version of almost locality uses a common dense translation-invariant domain with : and each local approximant act on , and for every and integer there is such that for all . A local or almost-local operator is an interpolator for if is defined and the vector below is nonzero.
For fermionic fields, the corresponding operator net is a -graded field net: each local algebra splits as and has a grading automorphism with for homogeneous , . Graded locality means for homogeneous and in spacelike separated regions. The graded net has the same isotony and translation covariance conditions. The local or almost-local interpolators used in that branch, their grading, and the statistics assignment are construction inputs.
denotes the fixed length represented by one numerical unit of the time parameter. A smooth compact momentum packet is a smooth compactly supported function ; its support is the closure of . Extend it to the bounded Borel function on and write for its bounded PVM integral. For a bounded interpolating operator , define the one-particle packet vector The integral is a bounded operator by the bounded Borel PVM integral theorem; it commutes with because both are functions of the same PVM. Its shell support lies in the compact Borel set , so the equivalent projection form is . The velocity support is . Packets have disjoint velocity supports when these sets are pairwise disjoint.
The associated scalar positive-energy packet solution, with fixed Fourier normalization, is For each fixed , this is smooth in and rapidly decreasing together with all spatial derivatives, meaning that for every and integer , where , . Indeed, the momentum integrand and all its derivatives are smooth and compactly supported, so repeated integration by parts in gives these bounds. Let for . For bounded local or almost-local , define the candidate smeared operator by the strong operator integral The rapid-decay estimate with is integrable on , since in spherical coordinates . For put Strong continuity of and boundedness of make continuous, with It is strongly measurable: on each , partition into finitely many half-open cubes of side , use the value of at each cube's lower corner, and set the simple function to zero outside the box. These simple functions converge pointwise to . The displayed majorant is integrable; the Bochner-integrability criterion therefore gives a Bochner integral for each . By the Bochner-integrable-function definition listed below, this integral is the norm limit of integrals of integrable simple approximants. Define . Linearity and the Bochner integral norm inequality give so this strong integral defines a bounded operator and
With the stated translation and Fourier conventions, its mass-shell component on is exactly . In fact, invariance of gives . For and any , the bounded linear functional passes through the Bochner integral by its simple-function definition. The spectral representation of , the polarization formula , and Fubini's theorem yield For each , use the finite positive scalar measure from the scalar and complex PVM-measures lemma listed below, which has total mass , and apply the sigma-finite Fubini theorem listed below to Lebesgue measure on and the finite positive Borel measure on . The product integrand is continuous and has absolute integral . Thus is bounded, and dominated convergence with majorant makes it continuous, hence Borel. Fourier inversion in the convention of the supplier listed under Definition references, after rescaling , gives Hence ; on this is . The PVM product identity follows first for simple functions and then by uniform approximation. Since , , and , the same identity gives Convergence of the full vector to that component is a separate construction obligation. For a domain-valued variant, the corresponding integrals and all products must instead be defined on the common invariant domain. Use the completed Hilbert tensor powers and their unitary permutation action: is the permutation group of and on elementary tensors. The sign is for an even permutation and for an odd permutation. The orthogonal symmetrizing and antisymmetrizing projections are and . For , the Fock space is the square-summable direct sum of the ranges of these projections for , together with vacuum sector at ; use the componentwise second-variable-linear inner product and vacuum conventions of the previously defined QFT Fock spaces, with for and for . The finite packet domain is the linear span of the vacuum and the -projections of elementary tensors built from with pairwise disjoint velocity supports. The selected value of and, for fermionic fields, any required graded locality are construction inputs.
For such a finite packet family , a candidate Haag–Ruelle approximant is , where is the dimensionless positive-time parameter, physical coordinate time is , and labels outgoing () or incoming () scattering. The operators act on a common dense domain invariant under translations and these operators, with ; every displayed product is required to be defined there. Bounded operator families are the special case . The operator families are supplied by the chosen construction. The one-particle limit condition is in norm as . On the zero-particle vacuum label , set for every . For each , the construction supplies a linear map whose values on elementary packet tensors are these operator products; the assignment must be well-defined independently of a tensor presentation. The Cook condition is that is norm- on and, for constants and , Norm- means that the norm derivative exists for each , has the corresponding one-sided derivative at , and is norm-continuous on . The parameter is the dimensionless numerical time in the fixed coordinate unit; changing that unit changes but not integrability. A construction must also establish any required convergence of approximant inner products to the specified inner products. The joint spectral input states cyclicity but not uniqueness of the invariant vacuum; any vacuum uniqueness or clustering hypothesis needed for this convergence must be stated or proved separately.
This is a contract for a proof, not an existence theorem. It does not derive the Cook bound, the one-particle limits, or the Fock inner-product limits from locality and shell isolation. An actual construction must also record uniform bounds on the vector approximants; those bounds are distinct from bounds on the operator factors .
Definition references
The Axiom of Countable Choice ()
Unital star algebra and positive normalized state
Positive-energy joint spectral input
Scalar future mass shell, invariant measure and test restriction
Schwartz/distribution spaces and Hilbert Fock conventions
Strongly measurable Banach-valued function
Bochner integrability criterion
Bochner integral norm inequality
Scalar and complex measures from a pvm
Fubini's theorem for L^1 functions on a sigma-finite product
Remarks
Charged quantum electrodynamics is outside this isolated massive charged-shell contract: massless photons and infraparticle sectors can invalidate its shell hypothesis. An infraparticle here means a charged excitation whose mass distribution has no isolated mass-shell eigen-subspace because of arbitrarily soft massless radiation. Lehmann–Symanzik–Zimmermann reduction (LSZ) is a separate route from distributional asymptotic fields and pole residues; this contract does not supply those fields, residues, or their domain arguments. Haag's no-go theorem concerns an exact unitary interaction-picture identification under its own hypotheses; it is a separate theorem obligation and is not a conclusion about finite-regulator Dyson evolution here.
Integrable derivatives yield scattering vectors
Statement
Let and the direction-labelled packet families be as in the massive scattering approximant contract, with , , and . Assume that for each fixed , the map is continuously differentiable in Hilbert-space norm and for constants and . Then the norm limit exists and In particular, each approximant family is uniformly bounded in norm. Write for the first-variable-linear pairing corresponding to the QFT Fock definition's second-variable-linear pairing. If is linear on and its pairwise first-variable inner products converge to , then is an isometry on and extends uniquely to an isometry on its Hilbert-space closure. The derivative estimate alone does not assert this inner-product convergence or that the range is all of .
Statement references
Facts & Assumptions
Given: A complete complex Hilbert space , a packet domain , a sign , continuously differentiable maps for that are linear in their packet label, and constants , satisfying the displayed derivative bound for every . For the isometry conclusion, also assume the stated pairwise inner-product limit.
Massive scattering packets and Cook approximant contract: the candidate families are Hilbert-space-valued norm- functions on each time half-line; their one-particle limits, smooth packet labels, and symmetric or antisymmetric packet-domain inner product are part of the construction data. The derivative and Fock inner-product estimates remain hypotheses of this theorem. The contract assumes Countable Choice.
Schwartz/distribution spaces and Hilbert Fock conventions: the bosonic and fermionic Fock spaces are square-summable direct sums of the symmetric and antisymmetric completed tensor sectors, with a second-variable-linear componentwise pairing. Its first-variable-linear counterpart is .
Fundamental theorem of calculus for Banach-valued continuous curves: under Countable Choice, for real , a real or complex Banach space , and a continuous curve that is differentiable on with derivative extending continuously to , the Bochner integral with respect to Lebesgue measure satisfies . The contract's Countable Choice assumption in [F1] supplies this hypothesis; a complex Hilbert space is a Banach space, and the contract's norm- condition supplies the required curve and derivative regularity on each compact interval.
Bochner integral norm inequality: for a Bochner-integrable Banach-valued function on a measurable set , . The continuous derivative in [F3] is Bochner integrable on .
For all , .
Proof
Fix . If the increment inequality is immediate. If , restrict to . By [F1] this is a continuous curve into the Banach space , differentiable on with derivative extending continuously to . The contract's Countable Choice premise satisfies the hypothesis of [F3], so the Banach-valued fundamental theorem gives . The derivative is continuous and hence Bochner integrable on this compact interval; [F4] then gives .
Apply the derivative bound in [F1] and integrate the scalar power: As , the last expression tends to zero uniformly for . Thus is Cauchy as ; completeness gives a limit . Taking in the first inequality gives the claimed rate, and taking gives for every .
For , linearity of each and norm convergence from 2.1 imply for all scalars : apply the triangle inequality to the finite linear combination and pass to the limit. Hence is linear on .
By continuity of the Hilbert inner product and the assumed limit [A1], . Setting proves preservation of norm, so is an isometry on .
If in converges in its Hilbert-space closure, then is Cauchy because . Completeness of defines a limit independent of the approximating sequence; the same equality passes to the limit. This is the unique isometric extension to . No surjectivity onto follows.
Scattering isometries do not establish asymptotic completeness
Statement
Let and let be the two isometric extensions supplied by the preceding Cook theorem after its pairwise Fock-inner-product hypothesis is proved. Define the comparison operator . Here the Hilbert adjoint of a bounded map is characterized by , a contraction satisfies for all , an isometry is a linear inner-product-preserving map, and unitary means a surjective isometry. Then is a contraction. It is unitary if and only if . Full asymptotic completeness is the stronger condition ; this stronger condition is not part of the unitary-on-common-range criterion.
Statement references
Facts & Assumptions
Given: The completed packet space , the physical Hilbert space , the isometric Cook maps .
Integrable derivatives yield scattering vectors: after the packet inner products are shown to converge to the Fock inner product, the norm limits extend to isometries on the completed packet domain. Cook convergence alone supplies no surjectivity statement.
Cauchy–Schwarz: , with equality exactly for linearly dependent vectors: in every complex Hilbert space.
Hilbert-adjoint identities: under Countable Choice, every
bounded linear map between real or complex Hilbert spaces has a unique bounded
Hilbert adjoint satisfying the adjoint identity; adjoints of compositions obey
. Its prerequisite chain supplies the Hilbert-adjoint
definition (def-hilbert-space-adjoint) and the Riesz representation result
(thm-riesz-representation-for-hilbert-space). The Countable Choice
hypothesis is already supplied by the scattering contract in [F1]. Since
are linear isometries, they are bounded, so their bounded
adjoints exist; after step 1.1, the same result applies to the bounded
comparison operator .
Proof
By [F3], the bounded linear isometry has a bounded Hilbert adjoint. For any in a Hilbert space, : Cauchy–Schwarz gives the upper bound, and if the choice attains it. For , the adjoint identity and [F2] therefore give , since . Therefore for every , so is a contraction.
By [F3], the bounded maps and have bounded Hilbert adjoints with the stated adjoint identities. For either isometry , the adjoint identity gives for all ; nondegeneracy therefore gives . For the same identity gives , so , and gives . Also fixes each and its image is contained in , so is the orthogonal projection onto the closed range. If , both products are the same projection . For all , , so uniqueness of the adjoint gives . It follows that and , so is unitary.
Conversely, suppose is unitary and put . By [F3] and step 1.2 this is a bounded orthogonal projection. For each , . For an orthogonal projection , the identity implies and hence ; therefore for every , proving . Since is onto, for every choose with . Then , which gives the reverse range inclusion. Thus the ranges coincide.
5 · Examples, experiments and counterexamples
None yet.