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.
Scalar future mass-shell measure and test restriction — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Areas of Elementary Plane Figures
- 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
- 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
- Fredholm Elliptic Problems and the Elliptic Spectrum
- 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
- Harmonic Functions and Mean Values in Rn
- 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
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Qm Math Composites
- Qm Math Oscillator
- 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
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Smooth Approximation and Sobolev Extension
- Smooth Partitions of Unity and Exhaustions
- Spacetime Primitives
- Spectral Measures and Borel Functional Calculus
- 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
- 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
- Unbounded Self Adjoint Operators and Stones Theorem
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Derivatives and Sobolev Spaces
2 · Summary
The example chooses nonnegative compactly supported tests in separated spacetime regions for the massless scalar representation. Their supports are spacelike separated, so the fields and local Weyl algebras commute, while the vacuum two-point pairing is strictly positive. The calculation is a mathematical correlation in the model and makes no statement about measurement, signaling, or empirical data.
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
Positive vacuum correlation for spacelike-separated massless tests
Example
Assume Countable Choice. In the massless model , there are nonnegative real test functions with spacelike-separated supports for which The corresponding local Weyl operators commute by Isotony and spacelike commutativity of scalar local Weyl algebras. The nonzero correlation is a mathematical vacuum expectation in the specified representation; it is not a measurement or a signaling effect.
Facts & Assumptions
Given: The massless shell measure and Fourier restriction of Scalar future mass shell, invariant measure and test restriction, the vacuum two-point formula of Smeared free scalar field and its Poincare representation, the causal and local-algebra results, and a smooth compactly supported nonnegative bump.
Assume Countable Choice. The Axiom of Countable Choice ()
For real tests the vacuum one-point function vanishes and . Smeared free scalar field and its Poincare representation
Spacelike-separated real tests have commuting fields and generate commuting local Weyl algebras. Causal support of the scalar commutator distribution Isotony and spacelike commutativity of scalar local Weyl algebras
The massless shell measure is , with phase . Scalar future mass shell, invariant measure and test restriction
Smooth compactly supported bumps exist in Euclidean balls. A smooth bump between concentric Euclidean balls
Dominated convergence applies to the integrable majorant below. Dominated convergence
Absolutely integrable functions on products of sigma-finite measure spaces may be integrated in either order. Fubini's theorem for L^1 functions on a sigma-finite product
The inner-product pairing satisfies Cauchy–Schwarz. Cauchy–Schwarz: , with equality exactly for dependent pairs
Verification
Choose . By [F4], choose a nonnegative nonzero . Choose two nonnegative nonzero supported in closed balls of radii whose center separation satisfies . Such bumps follow by translating and rescaling [F4]. Set and . For every point in the two supports, and ; therefore all support differences are spacelike. For example, , and give a spatial gap of , so these strict inequalities are attainable.
Insert a radial regulator , , in the massless two-point kernel. Angular integration using [F3] gives for and The integral identity follows by integrating the two exponentials in the sine and using . On the compact support product in 1.1, . Thus the denominator is bounded away from zero uniformly as , and converges uniformly there to , which is strictly positive.
The regulated shell integrals converge to by dominated convergence [F5]: the absolute value of the unregulated product is integrable by Cauchy–Schwarz [F7], because . To identify the regulated shell integral with the spacetime pairing of , Fubini [F6] applies because its absolute integral is at most . The formula in 2.1 and uniform convergence on the compact support product give because both test functions are nonnegative and nonzero and the denominator is positive on the support product. More explicitly, , since there. The zero one-point values follow from [F1]; commutation follows from [F2] and separation in step 1.1.