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.
Spacelike vacuum correlation without field commutator
A conditional calculation in the massless branch of the selected real scalar free model using compactly supported spacetime tests in strictly spacelike-separated regions. It reports no experiment or signaling result.
Example
In the massless branch , there are nonnegative real spacetime tests of unit with strictly spacelike-separated supports for which the vacuum two-point function is strictly positive, while the smeared field commutator and the commutator of the corresponding bounded local Weyl operators vanish. This is a state correlation in the selected model; it is not a measurement report or a signaling claim.
Facts & Assumptions
Given: Countable Choice, the massless branch and exact field conventions of Scalar distribution, covariance, locality and spectrum, and the stated measure and smooth-bump suppliers.
The Axiom of Countable Choice (): Countable Choice is the choice hypothesis carried by the selected free-field construction and polar-coordinate supplier.
Scalar distribution, covariance, locality and spectrum: for real spacetime tests, ; strictly spacelike-separated tests have vanishing field commutator and commuting bounded local Weyl algebras.
Scalar future mass shell, invariant measure and test restriction: for the shell density is away from the null apex, with phase .
A smooth bump between concentric Euclidean balls: for radii in , there is a smooth function valued in , equal to on the closed radius- ball and supported in the open radius- ball.
Cauchy-Schwarz inequality for : if , then .
Dominated convergence: almost-everywhere convergence under one integrable majorant gives convergence of the integrals.
Fubini's theorem for L^1 functions on a sigma-finite product: absolutely integrable functions on a sigma-finite product may be integrated in either order.
Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma: Lebesgue measure on decomposes as on radial coordinates.
A linear map of sends Lebesgue measurable sets to Lebesgue measurable sets, with when is invertible and Lebesgue null when it is not: an invertible linear map scales Lebesgue measure by the absolute determinant.
The polar surface set function on the unit sphere: the sphere surface measure is the radial projection measure used by the polar-coordinate supplier.
Sphere integrals in angle coordinates: for the stated spherical chart, and .
Verification
Given: [A1] and [F1]–[F10].
Fix metres, let metres, and take centers and in the stated length coordinates. Apply [F3] with radii and in , then translate the resulting bump to the two centers. This gives real dimensionless bumps valued in , each equal to on a nonempty inner ball and supported in and respectively. Define and , so both tests have unit . For any in these supports, and ; hence every support difference is spacelike.
Put and for metres damp the massless shell kernel by , so . By [F10] the spherical chart has surface element and ; combining this with [F7] gives and for with units ; each ball has finite shell measure, so the shell measure is sigma-finite. For a support difference , step 1.1 gives . Rotate coordinates so the third axis is ; the determinant-one rotation preserves Lebesgue measure and by [F8]. The angular integral is by [F10]. Thus . With and , writing the sine as exponentials and using for gives . Therefore .
For every , the shell/spacetime integrand paired with is absolutely integrable: compact support gives finite , and the radial measure calculation in step 2.1, [F2] and [F7] gives . Fubini [F6] therefore identifies the damped pairing with .
The shell vectors in [F1] lie in , so Cauchy–Schwarz [F4] gives . As , almost everywhere on the shell and is bounded by ; dominated convergence [F5] therefore makes the damped shell pairing converge to .
The set of support differences from step 1.1 is compact, and has a strictly positive lower bound there. The explicit formula in step 2.1 consequently converges uniformly on that set to . Taking the limit in the absolutely integrable pairing of step 3.1 and using step 4.1 and the vacuum covariance [F1] yields . The integral is finite because its denominator is bounded away from zero on the compact support product. By [F2] the kernel has units ; with tests of unit , the double integral and vacuum correlation are dimensionless.
The kernel in step 5.1 is strictly positive throughout the support product, and each test equals on a nonempty ball, so the integral is strictly positive. By [F1] the same tests have zero field commutator and their bounded local Weyl operators commute. A nonzero vacuum two-point function is thus compatible with spacelike commutativity in this model.
Depends on
Scalar distribution, covariance, locality and spectrum
Scalar future mass shell, invariant measure and test restriction
The Axiom of Countable Choice ()
A smooth bump between concentric Euclidean balls
Cauchy-Schwarz inequality for
Dominated convergence
Fubini's theorem for L^1 functions on a sigma-finite product
Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma
A linear map of sends Lebesgue measurable sets to Lebesgue measurable sets, with when is invertible and Lebesgue null when it is not
The polar surface set function on the unit sphere
Sphere integrals in angle coordinates