ExampleConstruction: AI-adaptedVerification: AI-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.

A boost-Killing congruence in flat space: acceleration source and conservation of the redshift-weighted energy current

Example

Let $M = R^{4}$ carry the identity chart, the flat metric $g = diag (- 1, 1, 1, 1)$ and the time orientation $N = \partial_{0}$ , with the standard coordinate orientation $d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ , and metric-selected connection $\nabla$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Metric compatibility, torsion freedom and the metric-selected connection class, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields). Let

$U : = {p \in M : x^{1} (p) > ∣ x^{0} (p) ∣}, ξ : = x^{1} \partial_{0} + x^{0} \partial_{1},$

let $X : = \sqrt{(x^{1})^{2} - (x^{0})^{2}} > 0$ on $U$ , let $n : = ξ / X$ , and let $T^{a b} : = ρ \partial_{0}^{a} \partial_{0}^{b}$ with $ρ > 0$ constant (the tensor of the dust model $(ρ, \partial_{0})$ , The dust matter model: rest density, four-velocity, stress-energy and dust system). Then:

$U$ is open, $ξ$ is a Killing field on $U$ , and $n$ is a smooth future-directed observer congruence on $U$ with $n^{a} \nabla_{a} X = 0$ and acceleration and expansion

$a = \nabla \ln X = \frac{x^{0}}{X^{2}} \partial_{0} + \frac{x^{1}}{X^{2}} \partial_{1}, θ = 0.$

$(ρ, \partial_{0})$ satisfies the dust system and $\nabla^{a} T_{a b} = 0$ on $M$ .
The measured fields of The observer split of a symmetric two-tensor: energy density, energy-momentum current, flux and stress for the congruence $n$ are

$μ = ρ \frac{(x^{1})^{2}}{X^{2}}, J = ρ \frac{x^{1}}{X} \partial_{0}, Φ = - ρ \frac{x^{1} (x^{0})^{2}}{X^{3}} \partial_{0} - ρ \frac{(x^{1})^{2} x^{0}}{X^{3}} \partial_{1} .$

$\nabla_{a} J^{a} = - Φ^{a} a_{a} = ρ x^{0} x^{1} / X^{3}$ and $D μ + μ θ + \nabla_{a} Φ^{a} = ρ x^{0} x^{1} / X^{3}$ : the balance of Divergence of the measured energy-momentum current and the finite-chain balance identity clause (b) holds with a nonvanishing acceleration source, so the measured energy current is not conserved.
$X J = ρ x^{1} \partial_{0}$ satisfies $\nabla_{a} (X J^{a}) = 0$ and $T^{a b} ξ_{b} = - X J^{a}$ : the redshift-weighted current is conserved, in accordance with Kinematics of a timelike Killing congruence and conservation of the redshift-weighted energy current clause (d). Consequently, for every finite smooth singular $4$ -chain $C \subseteq U$ with $\partial C = Σ_{2} - Σ_{1} + B$ , the flux $Φ_{X J}$ satisfies $Φ_{X J} (Σ_{2}) - Φ_{X J} (Σ_{1}) = - Φ_{X J} (B)$ ; in particular $Φ_{X J} (Σ_{2}) = Φ_{X J} (Σ_{1})$ whenever the velocity vectors of every simplex of $B$ span a hyperplane containing $\partial_{0}$ .

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g)$ with identity chart, $g = diag (- 1, 1, 1, 1)$ , metric-selected connection $\nabla$ , time orientation $N = \partial_{0}$ and standard coordinate orientation; the open set $U$ ; the vector field $ξ = x^{1} \partial_{0} + x^{0} \partial_{1}$ , the positive function $X = \sqrt{(x^{1})^{2} - (x^{0})^{2}}$ and the congruence $n = ξ / X$ ; the constant $ρ > 0$ and the tensor $T^{a b} = ρ \partial_{0}^{a} \partial_{0}^{b}$ .

[L1]

On the identity chart the Christoffel symbols vanish and $\nabla$ is the coordinate connection, so for smooth fields the covariant derivatives are the coordinate derivatives; in particular the divergence of a vector field is the coordinate divergence (Metric compatibility, torsion freedom and the metric-selected connection class, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, The inverse metric, musical isomorphisms and index raising).

[L2]

For a smooth vector field $ξ$ and a covariant $2$ -tensor field with constant chart components, $(L_{ξ} g)_{a b} = g_{c b} \partial_{a} ξ^{c} + g_{a c} \partial_{b} ξ^{c}$ ; $ξ$ is Killing exactly when $L_{ξ} g = 0$ (The coordinate formula for the Lie derivative of a covariant tensor, Killing fields of a Lorentzian metric).

[L3]

$U$ is open and on $U$ both $X > 0$ and $ξ$ is timelike and future-directed: $g (ξ, ξ) = - (x^{1})^{2} + (x^{0})^{2} = - X^{2}$ and $g (ξ, N) = - x^{1} < 0$ ; hence $n = ξ / X$ satisfies $g (n, n) = - 1$ , $g (n, N) = - x^{1} / X < 0$ and is a smooth observer congruence (Observer congruences, their observer curves and adapted charts, Observers, rest spaces and the spatial projection at an event, Timelike, null, spacelike and causal vectors of a Lorentz vector space, Real powers for positive bases, with the zero-base positive-exponent convention, Continuity and derivatives of positive-base real powers).

[L4]

For such a timelike Killing field one has $n^{a} \nabla_{a} X = 0$ , $a = \nabla \ln X$ and $θ = 0$ (Kinematics of a timelike Killing congruence and conservation of the redshift-weighted energy current clauses (a) and (b)).

[L5]

$(ρ, \partial_{0})$ is a dust model with tensor $T^{a b} = ρ \partial_{0}^{a} \partial_{0}^{b}$ ; the dust system holds for constant $ρ$ and constant $\partial_{0}$ , and it is equivalent to $\nabla^{a} T_{a b} = 0$ (The dust matter model: rest density, four-velocity, stress-energy and dust system, Divergence-free dust is exactly the dust system, and divergence-free perfect fluid is exactly the fluid equations clause (a)).

[L6]

The measured fields satisfy $J = μ n + Φ$ and the decomposition of The orthogonal observer decomposition of a symmetric two-tensor and its uniqueness; with $\nabla^{a} T_{a b} = 0$ the identities $\nabla_{a} J^{a} = - T^{a b} \nabla_{a} n_{b}$ and $D μ + μ θ + \nabla_{a} Φ^{a} = \nabla_{a} J^{a}$ hold (The observer split of a symmetric two-tensor: energy density, energy-momentum current, flux and stress, Divergence of the measured energy-momentum current and the finite-chain balance identity clauses (a) and (b)).

[L7]

For a timelike Killing field $ξ$ with $X = \sqrt{- g (ξ, ξ)}$ and $n = ξ / X$ : $T^{a b} \nabla_{a} n_{b} = Φ^{a} a_{a}$ , $\nabla_{a} (X J^{a}) = 0$ , $T^{a b} ξ_{b} = - X J^{a}$ , and the flux balance $Φ_{X J} (Σ_{2}) - Φ_{X J} (Σ_{1}) = - Φ_{X J} (B)$ holds on chains contained in $U$ (Kinematics of a timelike Killing congruence and conservation of the redshift-weighted energy current clauses (c) and (d)).

Verification

technique · direct; check the Killing equation in the identity chart, verify the unit and future conditions of $n$, compute the measured fields and the balance explicitly, and identify the divergence-free weighted current

1.1L2algebra

(Killing field.) In the identity chart the components of $g$ are constant, so [L2] gives $(L_{ξ} g)_{00} = 2 g_{00} \partial_{0} ξ^{0} = 2 (- 1) (0) = 0$ , $(L_{ξ} g)_{11} = 2 g_{11} \partial_{1} ξ^{1} = 2 (1) (0) = 0$ , $(L_{ξ} g)_{01} = g_{11} \partial_{0} ξ^{1} + g_{00} \partial_{1} ξ^{0} = 1 \cdot 1 + (- 1) \cdot 1 = 0$ , and the remaining components vanish because $ξ^{2} = ξ^{3} = 0$ and the metric is diagonal with $\partial_{a} ξ^{0} = δ_{a}^{1}$ , $\partial_{a} ξ^{1} = δ_{a}^{0}$ . Hence $L_{ξ} g = 0$ and $ξ$ is Killing on $M$ , hence on $U$ .

1.2L3L4algebra

(The congruence and its kinematics.) $U$ is open as the preimage of $(0, \infty)$ under the continuous function $x^{1} - ∣ x^{0} ∣$ . By [L3], $n = ξ / X$ is a smooth future-directed observer congruence on $U$ , and [L4] gives $n^{a} \nabla_{a} X = 0$ , $θ = 0$ and $a = \nabla \ln X$ ; since $\partial_{0} X = - x^{0} / X$ and $\partial_{1} X = x^{1} / X$ , the covector $a_{a} = \partial_{a} \ln X$ has components $(- x^{0} / X^{2}, x^{1} / X^{2})$ and the vector $a = (x^{0} / X^{2}) \partial_{0} + (x^{1} / X^{2}) \partial_{1}$ .

1.3L1L5algebra

(The dust model.) $ρ > 0$ is constant and smooth, and $\partial_{0}$ is a smooth future-directed unit timelike field with constant components; the dust system is $\nabla_{a} (ρ \partial_{0}^{a}) = ρ \partial_{0} (1) = 0$ and $\partial_{0}^{a} \nabla_{a} \partial_{0}^{b} = 0$ by [L1], so [L5] gives $\nabla^{a} T_{a b} = 0$ on $M$ .

2.1L1step 1.2L6algebra

(Measured fields.) By [L1], $n^{a} = (x^{1} / X) δ_{0}^{a} + (x^{0} / X) δ_{1}^{a}$ and $n_{a} = (- x^{1} / X) δ_{a}^{0} + (x^{0} / X) δ_{a}^{1}$ . Since $T_{a b} = ρ \partial_{a}^{0} \partial_{b}^{0}$ and $\partial_{0}^{a} n_{a} = n_{0} = - x^{1} / X$ , we get $μ = T_{a b} n^{a} n^{b} = ρ (x^{1})^{2} / X^{2}$ ; further $T^{a b} n_{b} = ρ \partial_{0}^{a} n_{0} = - ρ (x^{1} / X) \partial_{0}^{a}$ , so $J^{a} = - T^{a b} n_{b} = ρ (x^{1} / X) \partial_{0}^{a}$ and $Φ = J - μ n$ has components $Φ^{0} = ρ x^{1} / X - ρ (x^{1})^{2} / X^{2} \cdot x^{1} / X = - ρ x^{1} (x^{0})^{2} / X^{3}$ and $Φ^{1} = 0 - ρ (x^{1})^{2} / X^{2} \cdot x^{0} / X = - ρ (x^{1})^{2} x^{0} / X^{3}$ , using $(x^{1})^{2} - X^{2} = (x^{0})^{2}$ . This is clause 3, and the decomposition of [L6] holds by [L6].

3.1step 1.2step 2.1L1L6L7algebra

(The balance and its source.) By [L1] and step 2.1, $\nabla_{a} J^{a} = \partial_{0} ⁣ (ρ x^{1} / X) = ρ x^{1} \partial_{0} (X^{- 1}) = - ρ x^{1} X^{- 2} \partial_{0} X = ρ x^{0} x^{1} / X^{3}$ , using $\partial_{0} X = - x^{0} / X$ . On the other side, $Φ^{a} a_{a} = Φ^{0} (- x^{0} / X^{2}) + Φ^{1} (x^{1} / X^{2}) = ρ x^{1} (x^{0})^{3} / X^{5} - ρ (x^{1})^{3} x^{0} / X^{5} = ρ x^{0} x^{1} ((x^{0})^{2} - (x^{1})^{2}) / X^{5} = - ρ x^{0} x^{1} / X^{3}$ , so $\nabla_{a} J^{a} = - Φ^{a} a_{a}$ , consistent with [L7]. Moreover $D μ = n^{a} \partial_{a} μ = ρ [(x^{1} / X) (2 (x^{1})^{2} x^{0} / X^{4}) + (x^{0} / X) (2 x^{1} / X^{2} - 2 (x^{1})^{3} / X^{4})] = 2 ρ x^{0} x^{1} / X^{3}$ and $\nabla_{a} Φ^{a} = \partial_{0} Φ^{0} + \partial_{1} Φ^{1} = - ρ x^{0} x^{1} / X^{3}$ , so with $θ = 0$ the balance $D μ + μ θ + \nabla_{a} Φ^{a} = ρ x^{0} x^{1} / X^{3} = - Φ^{a} a_{a}$ of [L6] holds and its source does not vanish.

4.1step 1.2step 3.1L1L7algebra∎

(The weighted current and the flux balance.) $X J = ρ x^{1} \partial_{0}$ , so by [L1], $\nabla_{a} (X J^{a}) = \partial_{0} (ρ x^{1}) = 0$ ; and $T^{a b} ξ_{b} = ρ \partial_{0}^{a} \partial_{0}^{b} ξ_{b} = ρ \partial_{0}^{a} ξ_{0} = - ρ x^{1} \partial_{0}^{a} = - X J^{a}$ . Applying the flux balance of [L7] on $U$ with its induced standard orientation to $K = X J$ gives $Φ_{X J} (Σ_{2}) - Φ_{X J} (Σ_{1}) = - Φ_{X J} (B)$ for every finite smooth singular $4$ -chain $C \subseteq U$ with $\partial C = Σ_{2} - Σ_{1} + B$ . If the velocity vectors of every simplex of $B$ span a hyperplane containing $\partial_{0}$ , then $ι_{X J} {v o l}_{g}$ vanishes on those velocity vectors, because ${v o l}_{g} (\partial_{0}, v_{1}, v_{2}, v_{3}) = 0$ for linearly dependent arguments and $X J$ is a function multiple of $\partial_{0}$ ; hence $Φ_{X J} (B) = 0$ and $Φ_{X J} (Σ_{2}) = Φ_{X J} (Σ_{1})$ . This completes the verification.

Remarks

Contrast with the unweighted current. The measured energy current $J$ is not divergence-free: the boost congruence is accelerated, and clause 4 exhibits the source $- Φ^{a} a_{a}$ . The redshift weight $X$ converts $J$ into the divergence-free current $- T (\cdot, ξ)$ , which is the content of Kinematics of a timelike Killing congruence and conservation of the redshift-weighted energy current in this explicit model.
Interpretation of the weight. On $U$ the observers of the congruence move with rapidity $artanh (x^{0} / x^{1})$ relative to the static dust; $X = \sqrt{(x^{1})^{2} - (x^{0})^{2}}$ is the corresponding normalization, and the measured energy density $μ = ρ (x^{1})^{2} / X^{2}$ is the $γ^{2}$ -enhanced density of the static dust seen by them.
No measurement. The displayed values are exact identities of the flat model; the example asserts no measured value and no empirical claim.

A boost-Killing congruence in flat space: acceleration source and conservation of the redshift-weighted energy current

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources