LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Dust: conservation of rho n tensor n is equivalent to continuity and inertial flow

Statement

Let $Ω \subseteq A$ be open, let $ρ : Ω \to R$ be $C^{1}$ with $ρ > 0$ , let $n : Ω \to V$ be a $C^{1}$ field which is future timelike and satisfies $η (n, n) = - 1$ everywhere (a future unit timelike field, Norms of four-velocity and four-acceleration, and the observer rest-space decomposition,(c)), and set $T^{a b} : = ρ n^{a} n^{b}$ (a $C^{1}$ symmetric $(2, 0)$ field). Then, on $Ω$ , (a) $\partial_{a} T^{a b} = 0$ if and only if both $\partial_{a} (ρ n^{a}) = 0$ (continuity) and $n^{a} \partial_{a} n^{b} = 0$ (inertial flow); (b) if $ρ \geq 0$ is allowed to vanish, the implication $\partial_{a} T^{a b} = 0 \Rightarrow n^{a} \partial_{a} n^{b} = 0$ is asserted only on the open set ${ρ > 0}$ , and no assertion is made where $ρ = 0$ ; (c) Under the conservation hypothesis $\partial_{a} T^{a b} = 0$ in (a), if $J$ is an interval and $x : J \to Ω$ is a $C^{2}$ curve with $x^{'} (s) = n (x (s))$ for all $s$ (an integral curve of $n$ ), then $x^{''} (s) = 0$ : the flow lines of an inertial unit field are affine straight lines in the affine structure of $A$ . For the nonnegative-density branch in (b), the same conclusion holds for an integral curve whose image lies in ${ρ > 0}$ , under conservation there. The lemma is the exact mathematical content of the dust equations; it asserts no matter model, no interaction and no empirical fact. No choice principle is used.

Facts & Assumptions

Given: The affine Minkowski model $(A, V, η, C^{+})$ with fixed inertial chart $x$ and coordinate partial derivatives $\partial_{a}$ (Oriented time-oriented affine Minkowski space (the spacetime primitives), Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ), an open $Ω \subseteq A$ , $C^{1}$ fields $ρ : Ω \to R$ and $n : Ω \to V$ with $η (n, n) = - 1$ ; $n_{a} : = η_{a b} n^{b}$ and indices are raised and lowered with the constant $η$ (Norms of four-velocity and four-acceleration, and the observer rest-space decomposition,(c)). For a $C^{1}$ field $n$ the expression $n^{a} \partial_{a} n^{b}$ is the coordinate form of the flat covariant derivative $\nabla_{n} n$ (The flat covariant derivative on affine Minkowski space and fields along curves). For a $C^{1}$ symmetric type- $(2, 0)$ field $T$ one writes $f^{b} = \partial_{a} T^{a b}$ and calls $T$ conserved when $f = 0$ (C^k tensor fields on affine Minkowski space and their inertial components).

[F1]

Product rule for coordinate partial derivatives of products of $C^{1}$ functions: $\partial_{a} (ρ n^{a} n^{b}) = (\partial_{a} ρ) n^{a} n^{b} + ρ (\partial_{a} n^{a}) n^{b} + ρ n^{a} \partial_{a} n^{b}$ . (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ )

[F2]

If $I \subseteq R$ is an interval and $g : I \to R$ is continuous on $I$ and differentiable at every interior point with $g^{'} = 0$ there, then $g$ is constant on $I$ . (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant)

[F3]

Chain rule: a $C^{1}$ curve composed with a $C^{1}$ field is $C^{1}$ and its derivative is obtained by composing the derivative of the field with the curve derivative; concretely $\frac{d}{d s} n^{b} (x (s)) = \partial_{a} n^{b} (x (s)) x^{' a} (s)$ . (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ )

Proof

technique · direct

1.1F1given

Algebraic identity. Since $ρ$ and $n$ are $C^{1}$ , [F1] gives $\partial_{a} T^{a b} = \partial_{a} (ρ n^{a} n^{b}) = C n^{b} + ρ n^{a} \partial_{a} n^{b}$ with $C : = \partial_{a} (ρ n^{a})$ , the continuity expression.

1.2given

Contraction identity. Because $n_{b} n^{b} = η (n, n) = - 1$ is constant, its derivative vanishes: $0 = \partial_{a} (n_{b} n^{b}) = 2 n_{b} \partial_{a} n^{b}$ , hence multiplying by $n^{a}$ and summing, $n^{a} n_{b} \partial_{a} n^{b} = 0$ ; likewise $n_{b} C n^{b} = - C$ and $n_{b} n^{a} \partial_{a} n^{b} = 0$ .

2.1step 1.1step 1.2

Forward direction of (a) and clause (b). Assume $\partial_{a} T^{a b} = 0$ on $Ω$ . Contracting the identity of step 1.1 with $n_{b}$ and using step 1.2 gives $0 = C n_{b} n^{b} + ρ n_{b} n^{a} \partial_{a} n^{b} = - C$ , hence $C = 0$ . Substituting back gives $ρ n^{a} \partial_{a} n^{b} = 0$ for every $b$ . If $ρ > 0$ everywhere, division by $ρ$ gives $n^{a} \partial_{a} n^{b} = 0$ on $Ω$ ; if only $ρ \geq 0$ is assumed, the same conclusion holds on the open set ${ρ > 0}$ and no claim is made where $ρ = 0$ .

2.2step 1.1

Reverse direction of (a). Conversely, if $C = \partial_{a} (ρ n^{a}) = 0$ and $n^{a} \partial_{a} n^{b} = 0$ on $Ω$ , then step 1.1 gives $\partial_{a} T^{a b} = 0$ on $Ω$ .

3.1F2F3step 2.1

Clause (c). Let $x : J \to Ω$ be a $C^{2}$ curve with $x^{'} (s) = n (x (s))$ . By [F3], $x^{'' b} (s) = \partial_{a} n^{b} (x (s)) x^{' a} (s) = n^{a} \partial_{a} n^{b} (x (s))$ , which vanishes under the conservation hypothesis by step 2.1 (or, in the nonnegative-density branch, at every $s$ with $x (s) \in {ρ > 0}$ by step 2.1 applied there). Hence every component $(x^{b})^{'}$ has zero derivative at every interior point of $J$ , and [F2] gives that $(x^{b})^{'}$ is constant; applying [F2] to the function $s \mapsto x^{b} (s) - x^{b} (s_{0}) - (x^{b})^{'} (s_{0}) (s - s_{0})$ , whose derivative vanishes, gives $x^{b} (s) = x^{b} (s_{0}) + (x^{b})^{'} (s_{0}) (s - s_{0})$ for all $s \in J$ and every $b$ . Thus $x$ is an affine straight line and $x^{''} = 0$ on $J$ .

4.1step 2.1step 2.2step 3.1∎

Steps 2.1 and 2.2 prove (a), step 2.1 proves the restricted implication (b), and step 3.1 proves (c) and its branch on ${ρ > 0}$ . The argument is a pointwise component computation with the product rule and the constancy of $η (n, n)$ ; it asserts no matter model, no interaction, no dynamics of $ρ$ beyond the displayed equations and no empirical fact, and it uses no choice principle.

Dust: conservation of rho n tensor n is equivalent to continuity and inertial flow

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources