ExampleConstruction: AI-adaptedVerification: 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 locally conserved static uniaxial stress: tension must be constant along the stressed direction

Example

In an inertial chart $x$ of the affine Minkowski model with orthonormal basis $(e_{0}, e_{1}, e_{2}, e_{3})$ (Inertial frames and inertial charts of the affine Minkowski model), let $J \subseteq R$ be an interval (the range of the coordinate $x^{1}$ ) and let $ρ, P : J \to R$ be $C^{1}$ . Define the symmetric type- $(2, 0)$ field $T^{a b} (x) : = ρ (x^{1}) e_{0}^{a} e_{0}^{b} + P (x^{1}) e_{1}^{a} e_{1}^{b}$ on an open set $Ω$ whose $x^{1}$ -coordinates fill $J$ (a static uniaxial stress field along the $e_{1}$ direction, with $P < 0$ representing tension). For $Ω \neq \emptyset$ , this is a $C^{1}$ symmetric stress-energy field in the sense of Stress-energy tensor, force density and local balance on flat spacetime. If $Ω = \emptyset$ , then $J = \emptyset$ and the displayed formula defines the unique empty mathematical tensor field; the stress-energy and four-force terminology of that definition is not applied to this branch.

Facts & Assumptions

Given: The inertial chart $x$ with coordinate partials $\partial_{a}$ (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ), the interval $J$ , the $C^{1}$ functions $ρ, P$ , and the field $T$ above; in these components $e_{0}^{a} = δ_{0}^{a}$ and $e_{1}^{a} = δ_{1}^{a}$ . Write $D^{b} : = \partial_{a} T^{a b}$ for the coordinate divergence; for nonempty $Ω$ this is the four-force density $f^{b}$ of [F1].

[F1]

Force density and conservation terminology: on a nonempty open $Ω$ , for a $C^{1}$ symmetric type- $(2, 0)$ field $T$ , the four-force density is the field with components $f^{b} = \partial_{a} T^{a b}$ , and $T$ is locally conserved on $Ω$ exactly when $f = 0$ there. (Stress-energy tensor, force density and local balance on flat spacetime)

[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]

Constant functions have zero partial derivatives, and the coordinate partial derivatives are the derivatives of the corresponding one-variable restrictions. (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ )

Verification

technique · direct

1.1F3given

Components of the coordinate divergence. The components of $T$ are $T^{00} = ρ (x^{1})$ , $T^{11} = P (x^{1})$ and $T^{a b} = 0$ for all other pairs; these are $C^{1}$ in $x$ , so the coordinate divergence has components $D^{0} = \partial_{0} T^{00} + \partial_{1} T^{10} = \partial_{0} ρ (x^{1}) = 0$ , $D^{1} = \partial_{0} T^{01} + \partial_{1} T^{11} = P^{'} (x^{1})$ , and $D^{2} = D^{3} = 0$ , because the omitted terms involve the zero components and $ρ, P$ do not depend on $x^{0}$ .

2.1F1F2step 1.1

Vanishing coordinate divergence and constancy of $P$ . By construction the set of values $x^{1} (p)$ , $p \in Ω$ , is exactly the interval $J$ on which $ρ, P$ are defined. The set $J$ is open: a chart ball about any point of $x (Ω)$ permits all sufficiently small changes of its $x^{1}$ coordinate, hence a neighbourhood of each value in $J$ remains in $J$ ; this is also true when $J = \emptyset$ . Thus every point of $J$ is interior. By step 1.1, $D = 0$ on $Ω$ if and only if $P^{'} = 0$ at every interior point of $J$ ; by [F2] this holds if and only if $P$ is constant on $J$ . For nonempty $Ω$ , this is exactly local conservation by [F1]. For $Ω = J = \emptyset$ , $D = 0$ and constancy of the empty function $P$ are both vacuous, with any real constant, for example $0$ , witnessing constancy. The energy density $ρ$ is subject to no such condition: $ρ^{'}$ never enters the divergence, because the only term containing $ρ$ is $T^{00}$ , whose first index is contracted with $\partial_{0}$ and which is independent of $x^{0}$ .

3.1step 2.1∎

For nonempty $Ω$ , consequently, a static uniaxial stress in equilibrium has uniform stress $P$ along the stressed direction, while its energy density may vary; when $P < 0$ (tension) the tension must be constant. This is a component computation for the stated field; it asserts no material model, no equation of state and no force law.

Depends on

Dependency tree · 2 levels

Sources

B. Crowell, Special Relativity, revision 2020-12-10 (author-published undergraduate textbook, 246 PDF pages); signature (+---) converted to (-+++) and c = 1 formulas converted to x^0 = c t; Chapter 9 pp. 179-197: 9.1 pp. 179-182 (current vector, flux, charge conservation), 9.2 pp. 183-191 (stress-energy tensor, conservation and flux, symmetry, dust, rank-2 transformation law, pressure, perfect fluid, worked examples, energy conditions), 9.3 pp. 192-197 (Gauss's theorem, integral conservation laws, the energy-momentum vector, angular momentum); the printed 9.2.8 dominant energy condition p. 191 has the defective |P| > rho and is not used