LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Tetrad invariance of the future massive mass-shell measure

Statement

Let $x$ be an event of a time-oriented smooth Lorentzian four-manifold, let $M_{*} > 0$ , and let $e$ and $e^{'}$ be any two smooth future orthonormal tetrads near $x$ . The measures $d μ_{M_{*}, x, e}$ and $d μ_{M_{*}, x, e^{'}}$ defined in Canonical future massive mass-shell measure agree on every Borel subset of the future massive shell at $x$ . Hence the fiber measure $d μ_{M_{*}, x}$ is independent of the chosen future orthonormal tetrad.

Facts & Assumptions

Given: A future massive shell in one tangent space, mass energy $M_{*} > 0$ , two future orthonormal tetrads, and the countable-choice assumption carried by the cited change-of-variables supplier.

[F1]

In tetrad coordinates the shell is $P (q) = (E (q), q)$ , $E (q) = \sqrt{M_{*}^{2} + ∣ q ∣^{2}}$ , and its measure is $d^{3} q / E (q)$ (Canonical future massive mass-shell measure).

[F2]

If $e_{A}^{'} = B^{C}_{A} e_{C}$ , the basis-change theorem gives $B^{T} η B = η$ and $B^{0}_{0} > 0$ . Its inverse $Λ = B^{- 1}$ , which sends the first tetrad's component list to the second's, is also Lorentz and maps the chosen future timelike component and its massive shell onto themselves: $B$ maps the component into itself, and as an invertible linear map it maps that connected component onto the component containing $B e_{0}$ , which is the future one; the inverse has the same property. Taking determinants in $Λ^{T} η Λ = η$ gives $∣ \det Λ ∣ = 1$ (The change between two future-directed tetrads is a Lorentz matrix, Time orientation, future and past timelike/null/causal vectors, and the closed cones, The timelike set has exactly two convex components, described in orthonormal coordinates).

[F3]

If $Q : R^{3} \to R^{3}$ is a $C^{1}$ diffeomorphism, then for every nonnegative Borel $h$ , $\int h (q^{'}) d^{3} q^{'} = \int h (Q (q)) ∣ \det D Q (q) ∣ d^{3} q$ , assuming ${A C}_{ω}$ (Borel change of variables from the compact-support formula and Radon uniqueness, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1givenF1F2algebra

Write $P (q) = (E (q), q)$ in the first tetrad and let $q^{'} = Q (q)$ be the spatial coordinates of the same future-shell vector in the second tetrad. The tetrad change $Λ$ maps the entire future shell bijectively to itself; the spatial coordinate and its inverse are smooth, so $Q$ is a global $C^{1}$ diffeomorphism of $R^{3}$ . Form the $4 \times 4$ matrix $C (q) = [P (q), \partial_{1} P (q), \partial_{2} P (q), \partial_{3} P (q)]$ . Block elimination gives $\det C (q) = E (q) - ∣ q ∣^{2} / E (q) = M_{*}^{2} / E (q)$ .

2.1step 1.1F2algebra

The chain rule on the shell gives $Λ C (q) = C (q^{'}) diag (1, D Q (q))$ . Taking absolute determinants and using [F2] and step 1.1 yields $\frac{M_{*}^{2}}{E (q)} = \frac{M_{*}^{2}}{E (q^{'})} ∣ \det D Q (q) ∣, ∣ \det D Q (q) ∣ = \frac{E (q^{'})}{E (q)} .$

3.1step 2.1F3algebra∎

For any Borel $A$ on the shell, apply [F3] to the nonnegative Borel function $h (q^{'}) = 1_{A} (P_{e^{'}} (q^{'})) / E (q^{'})$ . Then $μ_{M_{*}, x, e^{'}} (A) = \int_{R^{3}} \frac{1_{A} (P_{e} (q))}{E (q^{'})} ∣ \det D Q (q) ∣ d^{3} q = \int_{R^{3}} \frac{1_{A} (P_{e} (q))}{E (q)} d^{3} q = μ_{M_{*}, x, e} (A),$ where the first equality uses the common geometric vector and the second uses step 2.1. This is equality of positive Borel measures, completing the proof.

Tetrad invariance of the future massive mass-shell measure

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources