TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Norms of four-velocity and four-acceleration, and the observer rest-space decomposition

Statement

Let $c > 0$ and let $(A, V, η, C^{+})$ be an oriented time-oriented affine Minkowski space (Oriented time-oriented affine Minkowski space (the spacetime primitives)).

(a) Norm of the four-velocity. Let $x : I \to A$ be a $C^{1}$ future timelike worldline with four-velocity $U$ (Four-velocity and four-acceleration of a future timelike worldline). Then $η (U (s), U (s)) = - c^{2}$ for every $s \in I$ ; equivalently the dimensionless four-velocity $u = U / c$ satisfies $η (u, u) = - 1$ , and $U (s)$ is future timelike. Thus the dimensionless four-velocity lies on the future unit hyperboloid ${v \in C^{+} : η (v, v) = - 1}$ .

(b) Orthogonality of the four-acceleration. If $x$ is $C^{2}$ at $s$ , then $η (U (s), A (s)) = 0$ : the four-acceleration has no component along the four-velocity; if in addition $A (s) \neq 0$ , then $A (s)$ is spacelike.

(c) Rest space and projection. Let $n \in V$ be future unit timelike, $η (n, n) = - 1$ , and put $n^{⊥} : = {v \in V : η (n, v) = 0}$ (eta-orthogonality and orthogonal complements in a Lorentz vector space). Then $n^{⊥}$ is a 3-dimensional linear subspace of $V$ , the restriction of $η$ to $n^{⊥}$ is positive definite, and the map $h : V \to V$ , $h (v) : = v + η (n, v) n$ , is linear, idempotent with $h \circ h = h$ , has image $n^{⊥}$ and kernel $span (n)$ , satisfies $h (n) = 0$ and $η (n, h (v)) = 0$ for all $v \in V$ , and every $v \in V$ has the unique decomposition $v = - η (n, v) n + h (v)$ . Moreover $∣ w ∣ : = \sqrt{η (w, w)}$ defines a norm on $n^{⊥}$ .

(d) Relative velocity and Lorentz factor. Let $n$ and $u$ be future unit timelike vectors, put $γ : = - η (n, u)$ and $w : = c h (u) / γ$ . Then $γ \geq 1$ , $w$ lies in $n^{⊥}$ , $u = γ (n + w / c)$ , $∣ w ∣^{2} = c^{2} (1 - γ^{- 2}) < c^{2}$ , $γ = (1 - ∣ w ∣^{2} / c^{2})^{- 1 / 2}$ , and $γ = 1$ if and only if $u = n$ . The vector $w$ is the velocity of a worldline with four-velocity $c u$ relative to the observer $n$ , and $γ$ is its Lorentz factor.

(e) Coordinate form. Let $(o; e_{0}, \dots, e_{3})$ be an inertial frame and let $y$ be a $C^{1}$ future timelike worldline whose inertial coordinates are $t \mapsto (c t, r (t))$ , with coordinate velocity $w (t) : = r^{'} (t)$ in $R^{3}$ and, when $y$ is $C^{2}$ , coordinate acceleration $a (t) : = w^{'} (t)$ . Then $∣ w (t) ∣ < c$ , the four-velocity is $U = γ_{w} (c, w)$ with $γ_{w} : = (1 - ∣ w ∣^{2} / c^{2})^{- 1 / 2}$ , and the four-acceleration is $A = γ_{w} \frac{d}{d t} (γ_{w} (c, w))$ , so that

$A^{0} = γ_{w}^{4} \frac{w \cdot a}{c}, A_{v e c} = γ_{w}^{2} a + γ_{w}^{4} \frac{(w \cdot a) w}{c^{2}};$

consequently $η (A, A) = γ_{w}^{4} ∣ a ∣^{2} + γ_{w}^{6} (w \cdot a)^{2} / c^{2} \geq 0$ , with $η (A, A) = 0$ if and only if $a = 0$ , and $η (U, A) = 0$ . For the observer $n = e_{0}$ of the chart, clauses (c) and (d) specialize to $γ = γ_{w}$ and $w_{r e l} = (0, w)$ in the frame coordinates, identified with $w$ via the spatial basis.

(f) Scope. The statement is a theorem about the affine Minkowski model with a fixed positive constant $c$ ; it asserts no clock reading and identifies no physical four-velocity. No choice principle is used.

Facts & Assumptions

Given: A real $c > 0$ and an oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ ; a $C^{1}$ future timelike worldline $x$ with four-velocity $U$ and (when $C^{2}$ ) four-acceleration $A$ ; a future unit timelike vector $n$ ; and, in clause (e), an inertial frame with coordinate path $t \mapsto (c t, r (t))$ .

[L1]

Four-velocity and four-acceleration (Four-velocity and four-acceleration of a future timelike worldline): $U = x^{'} / τ^{'}$ and, when $x$ is $C^{2}$ , $A = U^{'} / τ^{'}$ ; the dimensionless four-velocity is $u = U / c$ .

[L2]

Proper time (Proper time along a future timelike worldline, The proper-time function is a strictly increasing C^1 parametrization with C^1 inverse): $τ^{'} (s) = c^{- 1} \sqrt{- η (x^{'} (s), x^{'} (s))} > 0$ everywhere, and $x^{'}$ is future timelike.

[L3]

Bilinearity and symmetry of $η$ (Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space): $η$ is a symmetric bilinear form; $η (λ v, λ w) = λ^{2} η (v, w)$ .

[L4]

The future cone in orthonormal coordinates (The timelike set has exactly two convex components, described in orthonormal coordinates, Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones): in a future $η$ -orthonormal basis, $v$ is future timelike exactly when $v^{0} > ∣ v_{s p} ∣$ , timelike exactly when $η (v, v) < 0$ , spacelike exactly when $η (v, v) > 0$ , and the future timelike set is closed under multiplication by positive scalars.

[L5]

Orthogonal complements (eta-orthogonality and orthogonal complements in a Lorentz vector space): $S^{⊥} = {v : η (v, s) = 0 \forall s \in S}$ is a linear subspace, and $u \in u^{⊥}$ exactly when $η (u, u) = 0$ .

[L6]

Orthonormal bases (Every Lorentz form admits an ordered basis with matrix diag(-1,1,1,1)): there is an ordered $η$ -orthonormal basis with $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ ; one basis vector is timelike and the other three spacelike.

[L7]

Chart structure (Inertial frames and inertial charts of the affine Minkowski model, The Euclidean spatial structure and cross product of an inertial frame): in an inertial chart $η_{0} = diag (- 1, 1, 1, 1)$ ; the restriction $δ$ of $η$ to $S = span (e_{1}, e_{2}, e_{3})$ is the Euclidean form with norm $∣ \cdot ∣$ and inner product written $w \cdot z : = δ (w, z)$ ; $(e_{1}, e_{2}, e_{3})$ is a $δ$ -orthonormal basis.

[L8]

Linearity (Linear map between vector spaces over the same field): a map $h$ is linear when $h (λ v + μ w) = λ h (v) + μ h (w)$ .

[L9]

Cauchy-Schwarz (The Cauchy-Schwarz inequality for finite sums): for the positive definite form $δ$ , $∣ δ (u, v) ∣ \leq ∣ u ∣ ∣ v ∣$ , with equality exactly when $u, v$ are linearly dependent.

[L10]

Calculus (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$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Continuity and derivatives of positive-base real powers, Rational powers $a^{r}$ of a positive base, The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set): products and compositions of differentiable real functions obey the product and chain rules; $t \mapsto t^{α}$ is differentiable on $(0, \infty)$ with derivative $α t^{α - 1}$ ; and vector-valued derivatives are read componentwise.

[L11]

Ordered-field arithmetic (Complete ordered field (least-upper-bound property)): squares are nonnegative, a sum of nonnegative terms is nonnegative and vanishes exactly when all terms vanish, and positive quantities have positive inverses; order is total and transitive.

Proof

technique · direct

1.1givenL1L2L3L4

By [L1] and [L2], $U = x^{'} / τ^{'}$ with $τ^{'} = c^{- 1} \sqrt{- η (x^{'}, x^{'})} > 0$ ; hence $η (U, U) = η (x^{'}, x^{'}) / (τ^{'})^{2} = η (x^{'}, x^{'}) c^{2} / (- η (x^{'}, x^{'})) = - c^{2}$ by bilinearity [L3], and $u = U / c$ satisfies $η (u, u) = - c^{2} / c^{2} = - 1$ ; $U$ is a positive multiple of the future timelike $x^{'}$ , hence future timelike by [L4].

1.2givenL3L6L7

Fix an $η$ -orthonormal basis $(e_{0}, e_{1}, e_{2}, e_{3})$ with $e_{0}$ future (replace $e_{0}$ by $- e_{0}$ if necessary, using the cone description [L4]), write $n = n^{0} e_{0} + n_{s}$ and $v = v^{0} e_{0} + v_{s}$ with $n_{s}, v_{s} \in S$ , and use $η (n, n) = - (n^{0})^{2} + ∣ n_{s} ∣^{2} = - 1$ and $η (n, v) = - n^{0} v^{0} + n_{s} \cdot v_{s}$ from [L6], [L7], [L3].

1.3givenL1L2L4L7L10

In the chart of clause (e) the coordinate path is $t \mapsto (c t, r (t))$ , so its coordinate derivative is $(c, w (t))$ with $w = r^{'}$ by [L10], and $- η (x^{'}, x^{'}) = c^{2} - ∣ w (t) ∣^{2}$ by [L7]; since $x^{'}$ is future timelike, [L4] gives $c > ∣ w (t) ∣$ and $τ^{'} = c^{- 1} \sqrt{c^{2} - ∣ w ∣^{2}} = (1 - ∣ w ∣^{2} / c^{2})^{1 / 2} = 1 / γ_{w}$ ; hence $U = x^{'} / τ^{'} = γ_{w} (c, w)$ .

2.1step 1.2L4

For $n$ future unit timelike, [L4] gives $n^{0} > ∣ n_{s} ∣ \geq 0$ , and from $η (n, n) = - 1$ we get $(n^{0})^{2} = 1 + ∣ n_{s} ∣^{2} > 0$ , so $n^{0} > 0$ and division by $n^{0}$ is legitimate.

2.2step 1.1L1L2L3L10

If $x$ is $C^{2}$ at $s$ , then $U$ is differentiable at $s$ by [L1] and [L2] (a quotient of differentiable maps with positive denominator), and differentiating the constant $η (U, U) = - c^{2}$ of step 1.1 in an orthonormal basis gives $0 = \frac{d}{d s} η (U, U) = 2 η (U, U^{'})$ by the product rule [L10] and symmetry of $η$ ; since $A = U^{'} / τ^{'}$ with $τ^{'} > 0$ , this gives $η (U, A) = 0$ .

2.3step 1.2L4L9

For future unit timelike $n$ and $u$ , [L4] gives $n^{0} > ∣ n_{s} ∣$ and $u^{0} > ∣ u_{s} ∣$ in a future orthonormal basis of [L6]; hence $η (n, u) = - n^{0} u^{0} + n_{s} \cdot u_{s} \leq - n^{0} u^{0} + ∣ n_{s} ∣ ∣ u_{s} ∣ < 0$ by Cauchy-Schwarz [L9] (the last inequality because $n^{0} u^{0} > ∣ n_{s} ∣ u^{0} \geq ∣ n_{s} ∣ ∣ u_{s} ∣$ with at least one strict inequality), so $γ : = - η (n, u) > 0$ .

2.4step 1.3L10

If $y$ is $C^{2}$ , then $w$ is differentiable with derivative $a$ , $∣ w ∣^{2} = w \cdot w$ has derivative $2 w \cdot a$ by the product rule, and the chain rule with the power $t^{- 1 / 2}$ [L10] gives $\frac{d}{d t} γ_{w} = γ_{w}^{3} (w \cdot a) / c^{2}$ ; collecting terms in $A = γ_{w} \frac{d}{d t} (γ_{w} (c, w))$ gives $A^{0} = γ_{w}^{4} (w \cdot a) / c$ and $A_{v e c} = γ_{w}^{2} a + γ_{w}^{4} (w \cdot a) w / c^{2}$ .

3.1step 1.2step 2.1L9

For $v \in n^{⊥}$ , $η (n, v) = 0$ gives $v^{0} = (n_{s} \cdot v_{s}) / n^{0}$ , hence $η (v, v) = - (v^{0})^{2} + ∣ v_{s} ∣^{2} = ∣ v_{s} ∣^{2} - (n_{s} \cdot v_{s})^{2} / (n^{0})^{2} \geq ∣ v_{s} ∣^{2} (1 - ∣ n_{s} ∣^{2} / (n^{0})^{2}) = ∣ v_{s} ∣^{2} / (n^{0})^{2} \geq 0$ by Cauchy-Schwarz [L9] and the identity $(n^{0})^{2} = 1 + ∣ n_{s} ∣^{2}$ ; if $η (v, v) = 0$ then $∣ v_{s} ∣ = 0$ and $v^{0} = 0$ , so $v = 0$ : the restriction of $η$ to $n^{⊥}$ is positive definite.

3.2step 2.2step 1.3step 2.4L11

Expanding $η (A, A) = - (A^{0})^{2} + ∣ A_{v e c} ∣^{2}$ in the chart using step 2.4 and the identity $γ_{w}^{2} (1 - ∣ w ∣^{2} / c^{2}) = 1$ yields $η (A, A) = γ_{w}^{4} ∣ a ∣^{2} + γ_{w}^{6} (w \cdot a)^{2} / c^{2} \geq 0$ by [L11], with equality if and only if $a = 0$ (the first term vanishes only for $a = 0$ because $γ_{w} > 0$ ); and $η (U, A) = 0$ holds by step 2.2.

4.1step 1.2step 3.1L3L8

The map $φ : S \to n^{⊥}$ , $φ (v_{s}) : = v^{0} e_{0} + v_{s}$ with $v^{0} : = (n_{s} \cdot v_{s}) / n^{0}$ , is linear and bijective: linearity is clear from bilinearity of the inner product, injectivity from $v_{s} = 0 \Rightarrow v^{0} = 0$ , and surjectivity from step 3.1's computation of the first coordinate; hence $n^{⊥}$ is 3-dimensional.

4.2step 1.2step 3.1L3L5L8

The map $h (v) = v + η (n, v) n$ is linear by bilinearity [L3] and [L8]; $η (n, h (v)) = η (n, v) + η (n, v) η (n, n) = 0$ and $h (n) = n + η (n, n) n = 0$ ; $h (h (v)) = h (v) + η (n, h (v)) n = h (v)$ ; so $h$ is idempotent with image contained in $n^{⊥}$ and kernel containing $span (n)$ , and $v = - η (n, v) n + h (v)$ is a decomposition into $span (n)$ and $n^{⊥}$ , unique because those subspaces meet only in $0$ (a multiple $λ n$ with $η (n, λ n) = λ η (n, n) = - λ = 0$ vanishes); hence the image of $h$ is exactly $n^{⊥}$ and the kernel exactly $span (n)$ .

4.3step 3.1L3L11algebra

On $n^{⊥}$ , positive definiteness from step 3.1 gives $∣ w ∣ : = \sqrt{η (w, w)} \geq 0$ , with equality exactly for $w = 0$ , and bilinearity gives $∣ λ w ∣ = ∣ λ ∣ ∣ w ∣$ . For $z \neq 0$ , expand $0 \leq η (w - t z, w - t z)$ at $t = η (w, z) / η (z, z)$ to obtain $η (w, z)^{2} \leq η (w, w) η (z, z)$ ; the same inequality holds for $z = 0$ . Thus $∣ w + z ∣^{2} \leq (∣ w ∣ + ∣ z ∣)^{2}$ , and taking nonnegative square roots proves the triangle inequality. Hence this function is a norm on $n^{⊥}$ .

4.4step 1.1step 3.1step 2.2L4

If moreover $A (s) \neq 0$ , then $A (s) \in n^{⊥}$ for $n : = U (s) / c$ , a future unit timelike vector by step 1.1; the restriction of $η$ to $n^{⊥}$ is positive definite by step 3.1, so $η (A, A) > 0$ and $A (s)$ is spacelike by [L4].

5.1step 4.2step 4.3step 2.3L3L11

With $h$ of step 4.2, the decomposition $u = - η (n, u) n + h (u) = γ n + h (u)$ and bilinearity give $η (u, u) = γ^{2} η (n, n) + η (h (u), h (u)) = - γ^{2} + ∣ h (u) ∣^{2} = - 1$ ; since $∣ h (u) ∣^{2} \geq 0$ by positive definiteness on $n^{⊥}$ (step 4.3), $γ \geq 1$ , and with $w : = c h (u) / γ$ we get $∣ w ∣^{2} = c^{2} (γ^{2} - 1) / γ^{2} = c^{2} (1 - γ^{- 2}) < c^{2}$ ; also $u = γ n + h (u) = γ (n + w / c)$ and $(1 - ∣ w ∣^{2} / c^{2}) = γ^{- 2}$ , so $γ = (1 - ∣ w ∣^{2} / c^{2})^{- 1 / 2}$ by [L11].

6.1step 2.3step 5.1

Since $γ > 0$ and $u = γ n + h (u)$ , one has $γ = 1$ if and only if $h (u) = 0$ if and only if $u = n$ : if $u = n$ then $η (n, u) = η (n, n) = - 1$ so $γ = 1$ , and conversely $γ = 1$ forces $∣ h (u) ∣^{2} = γ^{2} - 1 = 0$ , hence $h (u) = 0$ by positive definiteness and $u = n$ .

6.2step 5.1step 1.3

For the observer $n = e_{0} = (1, 0, 0, 0)$ of the chart, $h (u) = u + η (e_{0}, u) e_{0} = u - u^{0} e_{0} = (0, u_{s})$ where $u_{s} = w / c γ_{w}$ by step 1.3, and $γ = - η (e_{0}, u) = u^{0} = γ_{w}$ ; hence $w_{r e l} = c h (u) / γ = (0, w)$ , the coordinate velocity, so clauses (c) and (d) specialize to $γ = γ_{w}$ and $w_{r e l} = (0, w)$ in the frame coordinates, identified with $w$ via the spatial basis.

7.1step 6.2∎

All arguments are finite-dimensional linear algebra and one-variable calculus in the given data; nothing is selected from a family and no choice principle is used.

Remarks

The hard part is clause (c). Positive definiteness of the restriction of $η$ to $n^{⊥}$ is where the signature hypothesis is spent; it is what makes $∣ h (u) ∣^{2} = γ^{2} - 1$ a nonnegative quantity and hence $γ \geq 1$ and $∣ w ∣ < c$ in clause (d), and it is also what makes a nonzero four-acceleration spacelike in clause (b).
The four-acceleration is not defined at kinks. Clause (b) assumes $x$ is $C^{2}$ at the point in question; no tangent or acceleration is asserted at a corner of a piecewise worldline, consistently with Total proper time of a piecewise C^1 future timelike worldline.

Norms of four-velocity and four-acceleration, and the observer rest-space decomposition

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources