ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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 dust solution with constant velocity and transverse density profile

Example

Let $∣ β ∣ < 1$ and $γ = (1 - β^{2})^{- 1 / 2}$ . Fix an inertial chart $x : A \to R^{4}$ and a positive $C^{1}$ map $ρ_{0} : R^{2} \to (0, \infty)$ . Let $n : A \to V$ be the constant field with components $n^{0} = γ$ , $n^{1} = γ β$ , $n^{2} = n^{3} = 0$ , and define $ρ : A \to (0, \infty)$ by $ρ (p) = ρ_{0} (x^{2} (p), x^{3} (p))$ . Then $(ρ, n)$ satisfies the dust equations and $T^{a b} = ρ n^{a} n^{b}$ is a conserved dust stress-energy field whose slice integrals over finite boxes are constant, even though its $x^{1}$ -face flux need not vanish.

Facts & Assumptions

Given: The affine Minkowski model with inertial chart $x$ and constant $η = diag (- 1, 1, 1, 1)$ (Oriented time-oriented affine Minkowski space (the spacetime primitives), Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space, Inertial frames and inertial charts of the affine Minkowski model); $∣ β ∣ < 1$ , $γ = (1 - β^{2})^{- 1 / 2} > 0$ (Rational powers $a^{r}$ of a positive base, Continuity and derivatives of positive-base real powers); the constant field $n = (γ, γ β, 0, 0)$ and the positive $C^{1}$ map $ρ_{0} : R^{2} \to (0, \infty)$ and its pullback $ρ (p) = ρ_{0} (x^{2} (p), x^{3} (p))$ ; $T = ρ n \otimes n$ .

[F1]

Dust equivalence: for a $C^{1}$ future unit timelike field $n$ and $C^{1}$ $ρ > 0$ , the field $T^{a b} = ρ n^{a} n^{b}$ is conserved, $\partial_{a} T^{a b} = 0$ , if and only if $\partial_{a} (ρ n^{a}) = 0$ and $n^{a} \partial_{a} n^{b} = 0$ ; under conservation every integral curve of $n$ is an affine straight line. If only $ρ \geq 0$ is assumed, the inertial-flow conclusion is asserted on ${ρ > 0}$ . (Dust: conservation of rho n tensor n is equivalent to continuity and inertial flow)

[F2]

Slice balance: $Q^{b} (s_{2}) - Q^{b} (s_{1}) = \int_{[s_{1}, s_{2}] \times \overset{ˉ}{K}} f^{b} d^{4} x - \sum_{i = 1}^{3} (\int_{[s_{1}, s_{2}] \times {\overset{ˉ}{K}}_{i}^{+}} T^{i b} - \int_{[s_{1}, s_{2}] \times {\overset{ˉ}{K}}_{i}^{-}} T^{i b})$ for finite boxes. (Finite-box stress balance and the flux form of conservation,(b), Stress-energy tensor, force density and local balance on flat spacetime)

[F3]

A constant field has vanishing partial derivatives, since each coordinate partial derivative is the derivative of a constant one-variable restriction. (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ )

Verification

technique · direct

1.1F1F3given

$(n, ρ)$ satisfies the dust equations. By the definitions of $γ$ and the Minkowski metric, $η (n, n) = - (n^{0})^{2} + (n^{1})^{2} = - γ^{2} (1 - β^{2}) = - 1$ , and $n^{0} = γ > 0$ in the chart's time orientation, so $n$ is a future unit timelike constant field; by [F3] $\partial_{a} n^{b} = 0$ and hence $n^{a} \partial_{a} n^{b} = 0$ . The profile depends only on $x^{2}, x^{3}$ , so $n^{a} \partial_{a} ρ = γ (\partial_{0} ρ + β \partial_{1} ρ) = 0$ ; and $\partial_{a} n^{a} = 0$ , so $\partial_{a} (ρ n^{a}) = n^{a} \partial_{a} ρ + ρ \partial_{a} n^{a} = 0$ . By [F1] the field $T^{a b} = ρ n^{a} n^{b}$ is conserved.

1.2F1given

Nonnegative variant and support. If $ρ_{0} \geq 0$ is allowed to vanish, the same equations $\partial_{a} (ρ n^{a}) = 0$ and $n^{a} \partial_{a} n^{b} = 0$ hold, and [F1] gives conservation, with the inertial-flow statement on ${ρ_{0} > 0}$ ; a compactly supported nonnegative transverse profile gives the same exact solution and the same finite-box constancy. The profile is independent of $x^{1}$ , so a nonzero profile is not compactly supported in all three spatial variables; the flow lines are $x^{1} = β x^{0} + const$ , $x^{2}, x^{3}$ constant.

2.1F2step 1.1

Finite slice integrals are constant. Let $\overset{ˉ}{K} = [c_{1}, d_{1}] \times [c_{2}, d_{2}] \times [c_{3}, d_{3}]$ with $c_{i} < d_{i}$ and $Q^{b} (s) = \int_{\overset{ˉ}{K}} T^{0 b} (s, x) d^{3} x$ . Since $T^{0 b} = ρ n^{0} n^{b} = γ n^{b} ρ_{0} (x^{2}, x^{3})$ is independent of $x^{0}$ , each $Q^{b} (s)$ is constant in $s$ . The same conclusion follows from [F2]: the force density vanishes by step 1.1, the transverse face terms vanish because $T^{2 b} = T^{3 b} = 0$ , and the two $x^{1}$ -faces carry the same pointwise integrand $T^{1 b} = ρ_{0} γ β n^{b}$ and enter with opposite signs, so their contributions cancel although the individual face flux need not vanish.

3.1step 1.1step 2.1step 1.2∎

The example exhibits a family of exact conserved dust solutions of the stated form with transverse profile and finite-box constancy of the slice integrals; it asserts no interaction, no dynamics of the profile beyond the displayed equations and no measurement.

A dust solution with constant velocity and transverse density profile

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels