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.

Dust in flat space: a conserved homogeneous model and a nonconserved time-dependent density

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 metric-selected connection $\nabla$ ; let $u : = \partial_{0}$ , a smooth future-directed unit timelike vector field on $M = R^{4}$ (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, A smooth vector field is a smooth section of the tangent bundle). Then:

For every smooth $ρ : R^{4} \to (0, \infty)$ with $\partial_{0} ρ = 0$ , the pair $(ρ, u)$ is a dust model on $M$ whose dust system holds and whose stress-energy tensor is divergence-free.
On the open subset $U : = {x \in R^{4} : x^{0} > - 1}$ the pair $(ρ ∣_{U}, u ∣_{U})$ with $ρ (t, x) = 1 + t$ is a dust model on $U$ whose dust system fails and whose stress-energy tensor has $\nabla^{a} T_{a b} = - δ^{0}_{b} \neq 0$ on $U$ .

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g)$ with identity chart, $g = diag (- 1, 1, 1, 1)$ , the unit field $u = \partial_{0}$ , and densities $ρ$ as in the two clauses.

[L1]

A dust model on an open $U$ is a pair $(ρ, u)$ with $ρ > 0$ smooth and $u$ smooth, future-directed, unit and timelike; its tensor is $T^{a b} = ρ u^{a} u^{b}$ and its system is $\nabla_{a} (ρ u^{a}) = 0$ , $u^{a} \nabla_{a} u^{b} = 0$ (The dust matter model: rest density, four-velocity, stress-energy and dust system, An open subset of a smooth manifold has a canonical restricted smooth structure).

[L2]

For every dust model with $ρ > 0$ , $\nabla^{a} T_{a b} = 0$ if and only if the dust system holds (Divergence-free dust is exactly the dust system, and divergence-free perfect fluid is exactly the fluid equations clause (a)).

[L3]

On the identity chart $Γ \equiv 0$ , so $\nabla$ is the coordinate connection and $\nabla_{a} V^{a} = \partial_{a} V^{a}$ for smooth vector fields (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).

Verification

technique · direct; compute the dust system and the divergence with the coordinate connection

1.1L1algebra

(The unit field is $\partial_{0}$ .) The field $u = \partial_{0}$ has constant components $(1, 0, 0, 0)$ , is smooth, satisfies $g (u, u) = - 1$ and $g (u, N) = - 1 < 0$ , so it is a future-directed unit timelike field by [L1].

2.1step 1.1L1L2L3algebra

(Conserved time-independent density.) Let $ρ > 0$ be smooth with $\partial_{0} ρ = 0$ . By [L3], $\nabla_{a} (ρ u^{a}) = \partial_{0} ρ = 0$ and $u^{a} \nabla_{a} u^{b} = \partial_{0} (δ^{b}_{0}) = 0$ : the dust system holds, so by [L2] $\nabla^{a} T_{a b} = 0$ . This is clause 1.

3.1step 1.1L1L2L3algebra∎

(Time-dependent density.) Let $ρ (t, x) = 1 + t$ , positive on the open set $U = {x^{0} > - 1}$ , and restrict $u$ to $U$ ; both restrictions are smooth on $U$ , and $u ∣_{U}$ remains future-directed, unit and timelike. By [L3] applied on $U$ , $\nabla_{a} (ρ u^{a}) = \partial_{0} ρ = 1 \neq 0$ , so the dust system fails; directly, $T^{a b} = (1 + t) δ^{a}_{0} δ^{b}_{0}$ and $\nabla_{a} T^{a b} = \partial_{0} (1 + t) δ^{0 b} = δ^{0 b}$ , and lowering the free index gives $\nabla^{a} T_{a b} = g_{b c} \nabla_{a} T^{a c} = - δ^{0}_{b}$ , which is nonzero on $U$ . This is clause 2, and it shows that the equivalence of [L2] is not vacuous.

Remarks

Physical reading. The conserved family is a constant dust congruence with time-independent, possibly spatially varying density in the flat model; the second family is not a solution of the dust system, and the field law of the framework would exclude it as a dust source. Neither statement is an empirical claim about matter.

Dust in flat space: a conserved homogeneous model and a nonconserved time-dependent density

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources