Pipeline-generated

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.

Proper Time Comparisons — Examples

1 · Prerequisites

2 · Summary

These examples and counterexamples work the proper-time page on explicit vectors and exact rationals. The reversed inequalities are evaluated on $(5, 3, 0, 0)$ and $(5, - 3, 0, 0)$ , giving $34 \geq 16$ strictly and the equality $32 = 4 \cdot 8$ for the proportional pair $(v, 2 v)$ , together with the reversed triangle instances $\sqrt{100} \geq 8$ and $\sqrt{91} \geq 9$ (Worked reverse Cauchy-Schwarz and reverse triangle inequalities); the boundary counterexample shows that the same-orientation hypotheses cannot be dropped, with the oppositely oriented timelike pair $(5, 3, 0, 0)$ , $(- 5, 3, 0, 0)$ violating the inequality and a spacelike pair failing the reversed spacelike inequality on a plane with no null direction (Counterexample: the reversed Cauchy-Schwarz inequality fails outside same-orientation timelike pairs). The rest-frame construction is worked for the displacement $(5, 3, 0, 0)$ : the frame basis $(5 / 4, 3 / 4, 0, 0)$ , $(3 / 4, 5 / 4, 0, 0)$ , $(0, 0, 1, 0)$ , $(0, 0, 0, 1)$ is verified orthonormal and the chart assigns $(4, 0, 0, 0)$ to the displacement (Worked rest frame of the future timelike displacement (5,3,0,0)).

The two-leg itinerary at speed $3 c / 5$ is compared with the straight clock: readings $8 T / 5$ and $2 T$ , difference $2 T / 5$ , in agreement with the strict endpoint bound, and the non-affine reparametrization $μ (s) = (s^{2} + s) / 2$ attains the bound, showing that equality does not require the affine parametrization (Worked two-leg itinerary against the straight clock at speed 3c/5). The counterexample $x (s) = p - s d$ shows that attaining the length bound with equality does not force the future orientation; future direction is imposed by the model's worldline and ideal-clock conventions (Counterexample: attainment of the endpoint bound does not force the future time orientation). Finally the traveler's two momentary rest frames are worked at $β = 3 / 5$ : their slices through the turn meet the stay-at-home worldline at $16 T / 25$ and $34 T / 25$ , a gap $18 T / 25 = 2 T v^{2} / c^{2}$ , and the reconciliation $16 T / 25 + 18 T / 25 + 16 T / 25 = 2 T$ reproduces the reunion reading, with relative boost parameter $15 / 17$ (Worked simultaneity gap of the traveler's two momentary rest frames at the turn).

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Worked reverse Cauchy-Schwarz and reverse triangle inequalities

Example

Worked computation in the chart $x$ of an inertial frame with $η_{0} = diag (- 1, 1, 1, 1)$ ; the vectors below are coordinate columns in the frame's basis.

(a) For $v : = (5, 3, 0, 0)$ and $w : = (5, - 3, 0, 0)$ one has $η (v, v) = η (w, w) = - 25 + 9 = - 16$ , so the timelike lengths are $\sqrt{16} = 4$ each, and $η (v, w) = - 25 - 9 = - 34$ , so $- η (v, w) = 34 \geq 4 \cdot 4 = 16$ ; the inequality is strict because $v$ and $w$ are not positive proportional.

(b) For $w^{'} : = 2 v = (10, 6, 0, 0)$ one has $η (w^{'}, w^{'}) = - 64$ and $\sqrt{- η (w^{'}, w^{'})} = 8$ , while $η (v, w^{'}) = - 50 + 18 = - 32$ , so $- η (v, w^{'}) = 32 = 4 \cdot 8$ : this is the equality case of the reversed Cauchy-Schwarz inequality, attained by the positive proportional pair $(v, 2 v)$ .

(c) Reverse triangle: $v + w = (10, 0, 0, 0)$ has $- η (v + w, v + w) = 100$ , so its root is $10 \geq 4 + 4 = 8$ , again strict because $v$ and $w$ are not positive proportional. For $u : = (5, 0, 0, 0)$ , of timelike length $5$ , one has $- η (v, u) = 25 \geq 4 \cdot 5 = 20$ and $v + u = (10, 3, 0, 0)$ with $\sqrt{- η (v + u, v + u)} = \sqrt{100 - 9} = \sqrt{91} \geq 4 + 5 = 9$ , since $91 > 81$ .

(d) Each of $v$ , $w$ , $w^{'}$ and $u$ is future timelike ( $5 > 3$ , $5 > 3$ , $10 > 6$ and $5 > 0$ in the first coordinate against the spatial norm), so all inequalities above are instances of the future timelike hypotheses of The reversed Cauchy-Schwarz inequality for future timelike vectors and The reversed triangle inequality and convexity of the future timelike cone.

Facts & Assumptions

Given: An inertial frame with chart $x$ and $η_{0} = diag (- 1, 1, 1, 1)$ , and the coordinate vectors $v = (5, 3, 0, 0)$ , $w = (5, - 3, 0, 0)$ , $w^{'} = (10, 6, 0, 0)$ , $u = (5, 0, 0, 0)$ (Inertial frames and inertial charts of the affine Minkowski model).

[L1]

Pairing in the frame: $η (r, r^{'}) = - r^{0} r^{' 0} + r^{1} r^{' 1} + r^{2} r^{' 2} + r^{3} r^{' 3}$ for coordinate vectors $r, r^{'}$ (Inertial frames and inertial charts of the affine Minkowski model, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

[L2]

Causal classification and cone coordinates: $r$ is timelike when $η (r, r) < 0$ , and in a frame with future first vector $r$ is future timelike exactly when $r^{0} > ∣ r_{s} ∣$ with $∣ r_{s} ∣ = \sqrt{(r^{1})^{2} + (r^{2})^{2} + (r^{3})^{2}}$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space, The timelike set has exactly two convex components, described in orthonormal coordinates).

[L3]

Reversed Cauchy-Schwarz inequality: for future timelike $r, s$ with $a = \sqrt{- η (r, r)}$ , $b = \sqrt{- η (s, s)}$ one has $- η (r, s) \geq a b$ , with equality exactly when $r$ and $s$ are positive proportional (The reversed Cauchy-Schwarz inequality for future timelike vectors).

[L4]

Reversed triangle inequality: for future timelike $r, s$ one has $r + s$ future timelike and $\sqrt{- η (r + s, r + s)} \geq \sqrt{- η (r, r)} + \sqrt{- η (s, s)}$ , with equality exactly when $r$ and $s$ are positive proportional (The reversed triangle inequality and convexity of the future timelike cone).

[L5]

Square roots and monotonicity: every real $c \geq 0$ has a unique $\sqrt{c} \geq 0$ with $(\sqrt{c})^{2} = c$ , so in particular $\sqrt{16} = 4$ ; for $x, y \geq 0$ one has $x < y ⟺ x^{2} < y^{2}$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Squaring is monotone on the nonnegatives).

[L6]

Elementary order arithmetic in $R$ : the order is trichotomous and transitive (Ordered field).

Verification

technique · direct

1.1givenL1algebra

Evaluating the diagonal form [L1] on the given coordinate vectors gives $η (v, v) = - 25 + 9 = - 16$ , $η (w, w) = - 25 + 9 = - 16$ , $η (w^{'}, w^{'}) = - 100 + 36 = - 64$ , $η (u, u) = - 25$ , $η (v, w) = - 25 - 9 = - 34$ , $η (v, w^{'}) = - 50 + 18 = - 32$ , $η (v, u) = - 25$ , $η (v + w, v + w) = η ((10, 0, 0, 0), (10, 0, 0, 0)) = - 100$ and $η (v + u, v + u) = - 100 + 9 = - 91$ .

2.1step 1.1L2algebra

By [L2] each of the four vectors is future timelike: $v^{0} = 5 > 3 = ∣ v_{s} ∣$ , $w^{0} = 5 > 3 = ∣ w_{s} ∣$ , $(w^{'})^{0} = 10 > 6 = ∣ (w^{'})_{s} ∣$ and $u^{0} = 5 > 0 = ∣ u_{s} ∣$ ; this is (d).

3.1step 1.1step 2.1L3L5L6algebra

For (a): $\sqrt{- η (v, v)} = \sqrt{- η (w, w)} = \sqrt{16} = 4$ by [L5], so the right-hand side is $16$ , while $- η (v, w) = 34$ ; the pair is not positive proportional, since $w = t v$ would give $t = 1$ from the first coordinates and then $- 3 = 3 t$ , a contradiction, and $v = t w$ fails the same way; hence the strict clause of [L3] gives $34 > 16$ , as claimed.

3.2step 1.1step 2.1L3L5algebra

For (b): $w^{'} = 2 v$ with $2 > 0$ , so the pair $(v, w^{'})$ is positive proportional; by the equality case of [L3] applied to the future timelike pair $(v, w^{'})$ one gets $- η (v, w^{'}) = \sqrt{- η (v, v)} \sqrt{- η (w^{'}, w^{'})}$ , and the values of step 1.1 give $\sqrt{- η (w^{'}, w^{'})} = \sqrt{64} = 8$ and $32 = 4 \cdot 8$ , the displayed equality.

4.1step 1.1step 2.1step 3.1L3L4L5algebra

For (c): the sum $v + w$ has the coordinate column $(10, 0, 0, 0)$ , so $- η (v + w, v + w) = 100$ and $\sqrt{100} = 10$ by [L5], and [L4] gives $10 \geq 4 + 4 = 8$ ; equality would force $v$ and $w$ positive proportional by [L4], which step 3.1 excludes, so the inequality is strict. Similarly $- η (v, u) = 25 \geq 4 \cdot 5 = 20$ with strictness by [L3] since $v$ and $u$ are not positive proportional, and $v + u$ has coordinate column $(10, 3, 0, 0)$ with $- η (v + u, v + u) = 91$ ; since $91 > 81 = 9^{2}$ with $9 \geq 0$ and $\sqrt{91} \geq 0$ , monotonicity of squaring on the nonnegatives [L5] gives $\sqrt{91} > 9 = 4 + 5$ .

5.1step 2.1step 3.1step 3.2step 4.1L3L4∎

Steps 3.1, 3.2 and 4.1 verify the strict, equality and strict reverse-triangle instances of (a), (b) and (c) respectively, all under the future timelike hypotheses confirmed in step 2.1; the equality case occurs exactly at the positive proportional pair of (b), in agreement with [L3] and [L4].

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Counterexample: the reversed Cauchy-Schwarz inequality fails outside same-orientation timelike pairs

Statement refuted

The following universal claim is false. Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski space.

(U1) The reversed Cauchy-Schwarz inequality $- η (v, w) \geq \sqrt{- η (v, v)} \sqrt{- η (w, w)}$ holds for every pair of vectors $v, w \in V$ that are individually timelike, regardless of their time orientations.

(U2) The analogous reversed form $∣ η (v, w) ∣ \geq \sqrt{η (v, v)} \sqrt{η (w, w)}$ holds for every pair of spacelike vectors $v, w \in V$ .

First witness, refuting (U1): in the inertial chart with diagonal metric $diag (- 1, 1, 1, 1)$ take $v : = (5, 3, 0, 0)$ , which is future timelike, and $w : = (- 5, 3, 0, 0)$ , which is past timelike. Then $η (v, w) = 34 > 0$ , so $- η (v, w) = - 34$ , while $\sqrt{- η (v, v)} \sqrt{- η (w, w)} = 4 \cdot 4 = 16$ , and the asserted inequality $- 34 \geq 16$ is false; the sum $v + w = (0, 6, 0, 0)$ is spacelike. Second witness, refuting (U2): $v : = (0, 1, 0, 0)$ and $w : = (0, 1, 1, 0)$ are spacelike with $η (v, v) = 1$ , $η (w, w) = 2$ , $η (v, w) = 1$ , so $∣ η (v, w) ∣ = 1 < 1 \cdot \sqrt{2} = \sqrt{η (v, v)} \sqrt{η (w, w)}$ . Hence the same-orientation hypothesis of The reversed Cauchy-Schwarz inequality for future timelike vectors cannot be dropped, and the spacelike reversed inequality is not universal.

Facts & Assumptions

Given: The oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ and an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with chart $x$ and coordinates $(u^{0}, u^{1}, u^{2}, u^{3})$ of a vector $u = u^{0} e_{0} + u^{1} e_{1} + u^{2} e_{2} + u^{3} e_{3}$ (Inertial frames and inertial charts of the affine Minkowski model).

[L1]

Coordinates and pairing: in the frame's ordered basis $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ , and by bilinearity $η (u, u^{'}) = - u^{0} u^{' 0} + u^{1} u^{' 1} + u^{2} u^{' 2} + u^{3} u^{' 3}$ for all $u, u^{'} \in V$ (Inertial frames and inertial charts of the affine Minkowski model, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

[L2]

Cone coordinates: $T_{+} = {u : u^{0} > ∣ u_{s} ∣}$ and $T_{-} = {u : u^{0} < - ∣ u_{s} ∣}$ are exactly the two components of the timelike set, and in a frame with $e_{0} \in C^{+}$ one has $C^{+} = T_{+}$ , $C^{-} = T_{-}$ ; hence $u$ is future timelike exactly when $u^{0} > ∣ u_{s} ∣$ and past timelike exactly when $u^{0} < - ∣ u_{s} ∣$ , where $∣ u_{s} ∣ = \sqrt{(u^{1})^{2} + (u^{2})^{2} + (u^{3})^{2}}$ (The timelike set has exactly two convex components, described in orthonormal coordinates, Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L3]

Causal classification: $u$ is timelike when $η (u, u) < 0$ , spacelike when $η (u, u) > 0$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L4]

The reversed Cauchy-Schwarz inequality and its equality case: for future timelike $v, w$ with $a : = \sqrt{- η (v, v)}$ , $b : = \sqrt{- η (w, w)}$ one has $- η (v, w) \geq a b$ , with equality exactly for positive proportional pairs; the same inequality holds for past timelike pairs (The reversed Cauchy-Schwarz inequality for future timelike vectors).

[L5]

Square roots and monotonicity of squaring: every real $c \geq 0$ has a unique $\sqrt{c} \geq 0$ with $(\sqrt{c})^{2} = c$ , in particular $\sqrt{1} = 1$ ; for $x, y \geq 0$ one has $x < y ⟺ x^{2} < y^{2}$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Squaring is monotone on the nonnegatives).

[L6]

Order of $R$ : the order is transitive, so $x < y < z$ implies $x < z$ (Ordered field).

Counterexample

technique · direct

1.1givenL1algebra

In the given inertial frame evaluate the four vectors of the two witnesses: $η (v, v) = - 25 + 9 = - 16 < 0$ and $η (w, w) = - 25 + 9 = - 16 < 0$ for $v = (5, 3, 0, 0)$ and $w = (- 5, 3, 0, 0)$ ; and $η (v, w) = 25 + 9 = 34$ for this pair; for the second pair $v^{'} = (0, 1, 0, 0)$ , $w^{'} = (0, 1, 1, 0)$ one has $η (v^{'}, v^{'}) = 1 > 0$ , $η (w^{'}, w^{'}) = 1 + 1 = 2 > 0$ and $η (v^{'}, w^{'}) = 1$ .

2.1step 1.1L2L3

Both $v$ and $w$ are timelike by [L3]; since $v^{0} = 5 > 3 = ∣ v_{s} ∣$ and $w^{0} = - 5 < - 3 = - ∣ w_{s} ∣$ , [L2] identifies $v$ as future timelike and $w$ as past timelike, so the pair $(v, w)$ is individually timelike with opposite time orientations.

2.2step 1.1L3L5algebra

For the second pair, [L3] makes $v^{'}$ and $w^{'}$ spacelike, and $\sqrt{η (v^{'}, v^{'})} \sqrt{η (w^{'}, w^{'})} = \sqrt{1} \cdot \sqrt{2} = 1 \cdot \sqrt{2} = \sqrt{2}$ by [L5]; since $1 < 2$ and $1, \sqrt{2} \geq 0$ , strict monotonicity of squaring gives $\sqrt{2} > 1$ ; hence $∣ η (v^{'}, w^{'}) ∣ = 1 < \sqrt{2} = \sqrt{η (v^{'}, v^{'})} \sqrt{η (w^{'}, w^{'})}$ , so (U2) is refuted.

2.3step 1.1L1algebra

The span of the second pair is ${(0, s, t, 0) : s, t \in R}$ , on which $η ((0, s, t, 0), (0, s, t, 0)) = s^{2} + t^{2}$ vanishes only for $s = t = 0$ : the subspace spanned by the two spacelike witnesses contains no null direction, so the failure of (U2) is not an artifact of a null direction in the span.

3.1step 1.1step 2.1L1L2L3algebra

The sum $v + w = (0, 6, 0, 0)$ has $η (v + w, v + w) = 36 > 0$ , so it is spacelike by [L3]. This is an additional property of this witness, not a criterion for failure of (U1): the pairing in (U1) and the causal character of the sum are distinct claims. Closure of the future timelike cone under addition does not apply here because $w$ is past timelike.

3.2step 1.1step 2.1L5L6algebra

For this pair $\sqrt{- η (v, v)} = \sqrt{16} = 4 = \sqrt{- η (w, w)}$ , so the right-hand side of (U1) is $16$ , while the left-hand side is $- η (v, w) = - 34 < 0$ ; since $0 < 16$ , transitivity gives $- 34 < 16$ , so $- 34 \geq 16$ is false and (U1) is refuted.

4.1step 3.1step 2.2step 2.3step 3.2L4∎

The two witnesses therefore refute the claimed universality: the reversed Cauchy-Schwarz inequality requires the same (future) time orientation of the pair, and the spacelike reversed form fails even on a spacelike plane with no null direction; neither witness contradicts the positive results [L4], which are stated for same-orientation timelike pairs.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Worked rest frame of the future timelike displacement (5,3,0,0)

Example

Worked computation in an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with $η_{0} = diag (- 1, 1, 1, 1)$ . Let $d : = (5, 3, 0, 0)$ , a future timelike coordinate vector with $- η (d, d) = 25 - 9 = 16$ , so $T : = \sqrt{- η (d, d)} = 4$ and $n : = d / T = (5 / 4, 3 / 4, 0, 0)$ .

(a) $n$ is future unit timelike: $η (n, n) = - 25 / 16 + 9 / 16 = - 1$ and $n^{0} = 5 / 4 > 3 / 4 = ∣ n_{s} ∣$ .

(b) The boost parameter $β : = n_{s} / n^{0} = (3 / 5, 0, 0)$ has $∣ β ∣ = 3 / 5 < 1$ and $γ = (1 - ∣ β ∣^{2})^{- 1 / 2} = 5 / 4$ , and the passive boost $B (β)$ of The passive Lorentz boost with parameter beta sends $n$ to $e_{0}$ , as clause (iv) of The passive boost is a proper orthochronous Lorentz map with inverse B(-beta) requires, since $γ (1, 3 / 5, 0, 0) = (5 / 4, 3 / 4, 0, 0) = n$ .

(c) The basis $(e_{0}^{'}, e_{1}^{'}, e_{2}^{'}, e_{3}^{'}) : = (n, B (- β) e_{1}, B (- β) e_{2}, B (- β) e_{3})$ has coordinate columns $e_{0}^{'} = (5 / 4, 3 / 4, 0, 0)$ , $e_{1}^{'} = (3 / 4, 5 / 4, 0, 0)$ , $e_{2}^{'} = (0, 0, 1, 0)$ , $e_{3}^{'} = (0, 0, 0, 1)$ ; the checks $η (e_{0}^{'}, e_{0}^{'}) = - 1$ , $η (e_{1}^{'}, e_{1}^{'}) = - 9 / 16 + 25 / 16 = 1$ , $η (e_{0}^{'}, e_{1}^{'}) = - (5 / 4) (3 / 4) + (3 / 4) (5 / 4) = 0$ , $η (e_{2}^{'}, e_{2}^{'}) = η (e_{3}^{'}, e_{3}^{'}) = 1$ and $η (e_{i}^{'}, e_{j}^{'}) = 0$ for the remaining pairs show that $(o; e_{0}^{'}, e_{1}^{'}, e_{2}^{'}, e_{3}^{'})$ is an inertial frame with first vector $n$ .

(d) Its chart $x^{'}$ assigns to $d$ the coordinates $(4, 0, 0, 0)$ : indeed $d = 4 n = 4 e_{0}^{'}$ , so $E^{' - 1} (d) = 4 E^{' - 1} (e_{0}^{'}) = (4, 0, 0, 0)$ ; in particular the two endpoints of any displacement $4 n$ have equal spatial coordinates in $x^{'}$ and time coordinates differing by $4$ .

Facts & Assumptions

Given: An inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with chart $x$ , $η_{0} = diag (- 1, 1, 1, 1)$ , the coordinate vector $d = (5, 3, 0, 0)$ , $T = \sqrt{- η (d, d)}$ , $n = d / T$ , and the boost parameter $β = n_{s} / n^{0}$ of The passive Lorentz boost with parameter beta (Inertial frames and inertial charts of the affine Minkowski model).

[L1]

Pairing in the frame: $η (r, r^{'}) = - r^{0} r^{' 0} + r^{1} r^{' 1} + r^{2} r^{' 2} + r^{3} r^{' 3}$ for coordinate vectors $r, r^{'}$ , and $η$ is symmetric and bilinear (Inertial frames and inertial charts of the affine Minkowski model, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

[L2]

Causal classification and cone: $r$ is timelike when $η (r, r) < 0$ and future timelike exactly when $r^{0} > ∣ r_{s} ∣$ in a frame with future first vector (Timelike, null, spacelike and causal vectors of a Lorentz vector space, The timelike set has exactly two convex components, described in orthonormal coordinates).

[L3]

Rest-frame lemma: for a future timelike displacement $d$ with $T = \sqrt{- η (d, d)}$ and $n = d / T$ , the vector $n$ is future unit timelike, and for every event $o$ there is an inertial frame with first vector $n$ ; in any such frame the chart assigns to $d$ the coordinates $(T, 0, 0, 0)$ (Existence of an inertial frame whose time axis is a prescribed future timelike direction).

[L4]

Boosts: for $β \in R^{3}$ with $0 < ∣ β ∣ < 1$ the passive boost $B (β)$ acts on coordinates by $x^{' 0} = γ (x^{0} - β \cdot x)$ , $x^{'} = x + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot x) β - γ β x^{0}$ , with $γ = (1 - ∣ β ∣^{2})^{- 1 / 2}$ ; for $β = 0$ set $B (0) = {id}_{V}$ ; for every $∣ β ∣ < 1$ , $B (β)$ is a proper orthochronous Lorentz map with inverse $B (- β)$ , and if $u$ is future unit timelike with coordinates $(u^{0}, u_{s})$ then $B (u_{s} / u^{0}) u = e_{0}$ ; for $β \cdot x = 0$ and $x^{0} = 0$ the formula returns $x$ (The passive Lorentz boost with parameter beta, The passive boost is a proper orthochronous Lorentz map with inverse B(-beta), Linear and affine Lorentz maps, and the Lorentz group).

[L5]

Square roots and monotonicity: every real $c \geq 0$ has a unique $\sqrt{c} \geq 0$ with $(\sqrt{c})^{2} = c$ , so $\sqrt{16} = 4$ and $\sqrt{9} = 3$ ; for $x, y \geq 0$ , $x < y ⟺ x^{2} < y^{2}$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Squaring is monotone on the nonnegatives).

[L6]

Order arithmetic: the order is trichotomous and transitive, and multiplication by a positive real preserves inequalities (Ordered field).

Verification

technique · direct

1.1givenL1L5algebra

By [L1], $η (d, d) = - 25 + 9 = - 16$ , so $- η (d, d) = 16 > 0$ and $T = \sqrt{16} = 4$ by [L5]; hence $n = d / T = (5 / 4, 3 / 4, 0, 0)$ and $n_{s} = (3 / 4, 0, 0)$ .

2.1step 1.1L1L2L3algebra

For (a): $η (n, n) = - (5 / 4)^{2} + (3 / 4)^{2} = - 25 / 16 + 9 / 16 = - 1$ by [L1], so $n$ is timelike, and $n^{0} = 5 / 4 > 3 / 4 = ∣ n_{s} ∣$ , so $n$ is future unit timelike by [L2] and [L3].

3.1step 2.1L4L5L6algebra

For (b): $β = n_{s} / n^{0} = (3 / 5, 0, 0)$ with $∣ β ∣ = 3 / 5$ and $∣ β ∣^{2} = 9 / 25 < 1$ , so $B (β)$ is defined; $γ = (1 - 9 / 25)^{- 1 / 2} = (16 / 25)^{- 1 / 2} = 5 / 4$ , because $(5 / 4)^{2} = 25 / 16$ and $5 / 4 > 0$ by [L5]; and $γ (1, 3 / 5, 0, 0) = (5 / 4) (1, 3 / 5, 0, 0) = (5 / 4, 3 / 4, 0, 0) = n$ , which is the displayed application of clause (iv) of [L4] to the future unit timelike vector $n$ .

4.1step 3.1L4L6algebra

For (c): the coordinate action of [L4] with parameter $- β$ gives $B (- β) e_{1}$ the column $(3 / 4, 5 / 4, 0, 0)$ : from $- β = (- 3 / 5, 0, 0)$ and $x = e_{1}$ , with spatial part $x_{v e c} = (1, 0, 0)$ , one gets $x^{' 0} = γ (x^{0} - (- β) \cdot x_{v e c}) = γ (0 + \frac{3}{5}) = \frac{5}{4} \cdot \frac{3}{5} = \frac{3}{4}$ and $x_{v e c}^{'} = x_{v e c} + \frac{γ - 1}{∣ β ∣^{2}} ((- β) \cdot x_{v e c}) (- β) - γ (- β) x^{0} = (1, 0, 0) + \frac{1 / 4}{9 / 25} \cdot (- \frac{3}{5}) \cdot (- \frac{3}{5}, 0, 0) = (1, 0, 0) + (\frac{1}{4}, 0, 0) = (\frac{5}{4}, 0, 0)$ , that is $B (- β) e_{1} = (3 / 4, 5 / 4, 0, 0)$ ; for $x = e_{2}$ and $x = e_{3}$ one has $β \cdot x = 0$ and $x^{0} = 0$ , so the formula returns $x$ , giving $B (- β) e_{2} = e_{2}$ and $B (- β) e_{3} = e_{3}$ ; and for $x = e_{0} = (1, 0, 0, 0)$ it gives $x^{' 0} = γ = 5 / 4$ and $x_{v e c}^{'} = - γ (- β) x^{0} = γ β = (3 / 4, 0, 0)$ , so $B (- β) e_{0} = (5 / 4, 3 / 4, 0, 0) = n = e_{0}^{'}$ ; these are the coordinate columns of the basis of the example, and $e_{a}^{'} = B (- β) e_{a}$ for every $a = 0, 1, 2, 3$ .

5.1step 4.1L1L2L3L4algebra

For the orthonormality checks of (c): $η (e_{0}^{'}, e_{0}^{'}) = - 25 / 16 + 9 / 16 = - 1$ , $η (e_{1}^{'}, e_{1}^{'}) = - 9 / 16 + 25 / 16 = 1$ , $η (e_{0}^{'}, e_{1}^{'}) = - (5 / 4) (3 / 4) + (3 / 4) (5 / 4) = 0$ , $η (e_{2}^{'}, e_{2}^{'}) = 1$ , $η (e_{3}^{'}, e_{3}^{'}) = 1$ , and the remaining cross pairings vanish by the diagonal form [L1]; since by step 4.1 the basis $(e_{0}^{'}, \dots, e_{3}^{'})$ is the image of the inertial basis $(e_{0}, \dots, e_{3})$ under the proper orthochronous Lorentz map $B (- β)$ of [L4], orthonormality also follows from metric preservation, the first vector $e_{0}^{'} = n$ is future timelike by step 2.1, and the basis is positively oriented because $B (- β)$ is proper and preserves the oriented volume form and the orientation class; therefore $(o; e_{0}^{'}, e_{1}^{'}, e_{2}^{'}, e_{3}^{'})$ is an inertial frame with first vector $n$ , as [L3] predicts.

6.1step 5.1L3algebra

For (d): $d = T n = 4 e_{0}^{'}$ by step 1.1 and step 4.1, so for the chart $x^{'} = E^{' - 1} (\cdot - o)$ of the frame of step 5.1 linearity gives $x^{'} (o + λ d) = E^{' - 1} (λ d) = λ E^{' - 1} (d) = λ (4, 0, 0, 0)$ because $E^{' - 1} (e_{0}^{'}) = (1, 0, 0, 0)$ ; in particular $x^{'}$ assigns to $d$ the coordinates $(4, 0, 0, 0)$ , and the two endpoints of any displacement $4 n$ have equal spatial coordinates and time coordinates differing by $4$ .

7.1step 2.1step 3.1step 4.1step 5.1step 6.1L3∎

Steps 2.1, 3.1, 5.1 and 6.1 verify (a), (b), (c) and (d) respectively: the example is the concrete instance $d = (5, 3, 0, 0)$ , $T = 4$ , $n = (5 / 4, 3 / 4, 0, 0)$ , $β = (3 / 5, 0, 0)$ of Existence of an inertial frame whose time axis is a prescribed future timelike direction, and the displayed basis is exactly the basis $e_{a}^{'} = B (- β) e_{a}$ constructed in step 4.1 and certified inertial in step 5.1.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Worked two-leg itinerary against the straight clock at speed 3c/5

Example

Worked computation in the inertial chart $x$ with metric $diag (- 1, 1, 1, 1)$ . Fix a real $c > 0$ . Let $T > 0$ , let $v$ with $0 < ∣ v ∣ < c$ and put $γ : = (1 - v^{2} / c^{2})^{- 1 / 2}$ ; let $p : = x^{- 1} (0, 0, 0, 0)$ , $r : = x^{- 1} (c T, v T, 0, 0)$ and $q : = x^{- 1} (2 c T, 0, 0, 0)$ , the parameter in each coordinate being the laboratory time $t$ in seconds, so that the coordinate columns displayed are those of the events in the chart with $x^{0} = c t$ .

(a) The straight worldline from $p$ to $q$ has displacement $d : = (2 c T, 0, 0, 0)$ , with $- η (d, d) = 4 c^{2} T^{2}$ and elapsed proper time $c^{- 1} 2 c T = 2 T$ .

(b) The two-leg itinerary $p \to r \to q$ , with the parameter on each leg in $[0, T]$ , has first-leg displacement $(c T, v T, 0, 0)$ with $- η = c^{2} T^{2} (1 - v^{2} / c^{2})$ , hence proper time $c^{- 1} c T \sqrt{1 - v^{2} / c^{2}} = T / γ$ , and second-leg displacement $(c T, - v T, 0, 0)$ with the same value; its two-leg total proper time is $2 T / γ$ .

(c) Comparison: $2 T / γ < 2 T$ for every $v$ with $0 < ∣ v ∣ < c$ , in agreement with the endpoint bound and with its strictness clause, since the image of the two-leg itinerary contains the event $r$ , which is not on the straight segment from $p$ to $q$ . Numerical specialization $v = 3 c / 5$ (so $γ = 5 / 4$ ): the readings are $8 T / 5$ and $2 T$ , with difference $2 T / 5$ .

(d) Equality without affine parametrization: on $[0, 1]$ let $μ (s) : = (s^{2} + s) / 2$ , a strictly increasing $C^{1}$ surjection of $[0, 1]$ onto itself with $μ^{'} (s) = s + 1 / 2 > 0$ ; the worldline $y (s) : = x^{- 1} (2 c T μ (s), 0, 0, 0)$ has the straight segment $p q$ as image and elapsed proper time $c^{- 1} \int_{0}^{1} 2 c T μ^{'} (s) d s = 2 T$ : equality in the endpoint bound does not require the affine parametrization, only a future-directed strictly increasing one.

Facts & Assumptions

Given: An inertial frame with chart $x$ and $η_{0} = diag (- 1, 1, 1, 1)$ ; a duration $T > 0$ in seconds and a speed $v$ with $0 < ∣ v ∣ < c$ ; $γ = (1 - v^{2} / c^{2})^{- 1 / 2}$ ; the events $p = x^{- 1} (0, 0, 0, 0)$ , $r = x^{- 1} (c T, v T, 0, 0)$ , $q = x^{- 1} (2 c T, 0, 0, 0)$ ; the two-leg coordinate itinerary $p \to r \to q$ and the reparametrized straight worldline $y (s) = x^{- 1} (2 c T μ (s), 0, 0, 0)$ with $μ (s) = (s^{2} + s) / 2$ (Inertial frames and inertial charts of the affine Minkowski model).

[L1]

Pairing in the frame: $η (r, r^{'}) = - r^{0} r^{' 0} + r^{1} r^{' 1} + r^{2} r^{' 2} + r^{3} r^{' 3}$ for coordinate columns, by the diagonal form and bilinearity; coordinate differences of events are the coordinates of their displacements (Inertial frames and inertial charts of the affine Minkowski model, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

[L2]

Cone coordinates (The timelike set has exactly two convex components, described in orthonormal coordinates, Timelike, null, spacelike and causal vectors of a Lorentz vector space): a vector $(w^{0}, w_{s})$ with $w^{0} > ∣ w_{s} ∣$ is future timelike.

[L3]

Straight and piecewise straight proper times (Proper time along a future timelike worldline, Total proper time of a piecewise C^1 future timelike worldline, Curves, regular causal curves and future timelike worldlines in affine Minkowski space, Inertial and piecewise inertial worldlines of the affine Minkowski model): a straight worldline with constant tangent $w$ over a parameter interval of length $L$ has proper time $c^{- 1} L \sqrt{- η (w, w)}$ ; the two-legged piecewise inertial itinerary has total proper time the sum of its leg values; and in the globally $C^{1}$ case the proper time is $c^{- 1} \int \sqrt{- η (x^{'}, x^{'})}$ in the oriented convention of The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ .

[L4]

Endpoint bound and strictness (The endpoint bound for proper time and the maximality of the straight worldline in affine Minkowski space): $c Δ τ (x) \leq \sqrt{- η (q - p, q - p)}$ for weak piecewise future timelike worldlines from $p$ to $q$ , with strict inequality whenever the image is not contained in the straight segment; equality holds for every strictly increasing reparametrization of the straight segment.

[L5]

Roots, powers and monotonicity (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Squaring is monotone on the nonnegatives, Rational powers $a^{r}$ of a positive base): every $a \geq 0$ has a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; for $x, y \geq 0$ , $x \leq y ⟺ x^{2} \leq y^{2}$ ; and $γ > 0$ satisfies $γ^{2} = (1 - v^{2} / c^{2})^{- 1}$ .

[L6]

Riemann calculus (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ): if $g$ is continuous on $[0, 1]$ with $G^{'} = g$ , then $\int_{0}^{1} g = G (1) - G (0)$ .

[L7]

Order arithmetic (Ordered field): the order is transitive and $0 < 1$ ; and $0 < ∣ v ∣ < c$ gives $0 < v^{2} / c^{2} < 1$ .

Verification

technique · direct

1.1givenL1L2L7algebra

By [L1] the displacement columns are $d = q - p = (2 c T, 0, 0, 0)$ , $r - p = (c T, v T, 0, 0)$ and $q - r = (c T, - v T, 0, 0)$ ; their interval values are $η (d, d) = - 4 c^{2} T^{2}$ , $η (r - p, r - p) = - c^{2} T^{2} + v^{2} T^{2} = - c^{2} T^{2} (1 - v^{2} / c^{2})$ , $η (q - r, q - r) = - c^{2} T^{2} (1 - v^{2} / c^{2})$ ; since $0 < ∣ v ∣ < c$ gives $c - ∣ v ∣ > 0$ , hence $c > ∣ v ∣$ , the time component of each of the three columns strictly dominates the Euclidean norm of its spatial part, and all three displacements are future timelike by [L2].

2.1step 1.1L3L5algebra

For (a): the straight worldline from $p$ to $q$ runs over a parameter interval of length $2 T$ with constant tangent $(c, 0, 0, 0)$ , whose interval value is $- c^{2}$ , so by [L3] its elapsed proper time is $c^{- 1} \cdot 2 T \cdot \sqrt{c^{2}} = 2 T$ , agreeing with the value $c^{- 1} \sqrt{- η (d, d)} = c^{- 1} 2 c T$ computed from the displacement.

2.2step 1.1L3L5algebra

For (b): each leg runs over a parameter interval of length $T$ with constant tangent $(c, \pm v, 0, 0)$ , whose interval value is $- c^{2} + v^{2} = - c^{2} (1 - v^{2} / c^{2})$ ; by [L3] each leg has proper time $c^{- 1} T \sqrt{c^{2} - v^{2}} = T \sqrt{1 - v^{2} / c^{2}} = T / γ$ , the last equality because $γ = (1 - v^{2} / c^{2})^{- 1 / 2} > 0$ ; the two-leg total is the sum $2 T / γ$ by the additivity clause of [L3].

2.3step 1.1L1L2L5algebra

For (d): $μ (0) = 0$ , $μ (1) = 1$ and $μ^{'} (s) = s + 1 / 2 > 0$ on $[0, 1]$ . For $0 \leq s < t \leq 1$ , $μ (t) - μ (s) = (t - s) (t + s + 1) / 2 > 0$ , proving strict increase; and for each $λ \in [0, 1]$ the value $s = (- 1 + \sqrt{1 + 8 λ}) / 2$ lies in $[0, 1]$ and satisfies $μ (s) = λ$ , proving surjectivity by [L5]. Thus $μ$ is a strictly increasing $C^{1}$ surjection of $[0, 1]$ onto itself; the worldline $y (s) = x^{- 1} (2 c T μ (s), 0, 0, 0)$ has parameter path $(2 c T μ (s), 0, 0, 0)$ with tangent $(2 c T μ^{'} (s), 0, 0, 0)$ , whose time component $2 c T μ^{'} (s)$ is positive and whose interval value is $- (2 c T μ^{'} (s))^{2}$ , so $y$ is a future timelike worldline by [L2] with $\sqrt{- η (y^{'}, y^{'})} = 2 c T μ^{'} (s)$ ; its image is ${x^{- 1} (2 c T λ, 0, 0, 0) : λ \in [0, 1]}$ , the straight segment from $p$ to $q$ .

3.1step 1.1step 2.2L4L5L7algebra

For (c): by [L7] $0 < v^{2} / c^{2} < 1$ , so $0 < 1 - v^{2} / c^{2} < 1$ and strict monotonicity of squaring on the nonnegatives gives $\sqrt{1 - v^{2} / c^{2}} < 1$ ; hence $1 / γ = \sqrt{1 - v^{2} / c^{2}} < 1$ and $2 T / γ < 2 T$ . This agrees with [L4]: the displacement $r - p = (c T, v T, 0, 0)$ has second coordinate $v T \neq 0$ because $v \neq 0$ and $T > 0$ , so $r$ is not on the straight segment from $p$ to $q$ (all of whose events have vanishing second coordinate), and the strictness clause of [L4] applies to the two-leg itinerary.

3.2step 2.1step 2.3L4L6algebra

Its elapsed proper time is $c^{- 1} \int_{0}^{1} 2 c T μ^{'} (s) d s = 2 T (μ (1) - μ (0)) = 2 T$ by [L6] applied to the continuous derivative $μ^{'}$ , so equality in the endpoint bound is attained although $μ$ is not affine; by [L4] this is consistent with the equality characterization, since $μ$ is a strictly increasing future-directed reparametrization of the straight segment.

4.1step 2.1step 2.2step 2.3step 3.1step 3.2L4∎

Clauses (a)-(d) are verified in steps 2.1, 2.2, 3.1, 3.2: the readings $2 T$ (straight) and $2 T / γ < 2 T$ (two-leg), the strict comparison, the numerical values $8 T / 5$ and $2 T$ at $v = 3 c / 5$ , and the non-affine equality case of (d) are all finite evaluations of the model's definitions.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Counterexample: attainment of the endpoint bound does not force the future time orientation

Statement refuted

The following claim is false: if a piecewise $C^{1}$ curve $x : [α, β] \to A$ with nonzero timelike tangents runs from an event $p$ to an event $q$ and attains the endpoint bound $\sqrt{- η (q - p, q - p)}$ in the length-integral sense, that is $\int_{α}^{β} \sqrt{- η (x^{'}, x^{'})} d s = \sqrt{- η (q - p, q - p)}$ , then its tangents must be future timelike, so that $x$ is a worldline of the model.

Counterexample: in the inertial chart $ξ$ with diagonal metric $diag (- 1, 1, 1, 1)$ let $d : = (5, 3, 0, 0)$ , a future timelike displacement with $\sqrt{- η (d, d)} = 4$ , and put $p : = ξ^{- 1} (0, 0, 0, 0)$ , $q : = ξ^{- 1} (- 5, - 3, 0, 0) = p - d$ and $x (s) : = p - s d$ for $s \in [0, 1]$ . Then $x (0) = p$ , $x (1) = p - d = q$ , and $x^{'} (s) = - d$ is past timelike for every $s$ , so $x$ is not a future timelike worldline; but its length integrand is $\sqrt{- η (- d, - d)} = \sqrt{- η (d, d)} = 4$ and its length integral over $[0, 1]$ equals $4$ , while $\sqrt{- η (q - p, q - p)} = \sqrt{- η (- d, - d)} = 4$ : the bound is attained with equality by a past-directed parametrization. Attainment of the length bound therefore does not force the future time orientation; the model's clock interpretation separately restricts its readings to future timelike worldlines (Proper time along a future timelike worldline, Curves, regular causal curves and future timelike worldlines in affine Minkowski space). Within the future timelike worldline class the equality case is characterized by The endpoint bound for proper time and the maximality of the straight worldline in affine Minkowski space (ii).

Facts & Assumptions

Given: An inertial frame with chart $ξ$ and $η_{0} = diag (- 1, 1, 1, 1)$ ; the coordinate vector $d = (5, 3, 0, 0)$ ; the events $p = ξ^{- 1} (0, 0, 0, 0)$ , $q = ξ^{- 1} (- 5, - 3, 0, 0)$ ; and the curve $x (s) = p - s d$ on $[0, 1]$ (Inertial frames and inertial charts of the affine Minkowski model).

[L1]

Pairing in the frame: $η (r, r^{'}) = - r^{0} r^{' 0} + r^{1} r^{' 1} + r^{2} r^{' 2} + r^{3} r^{' 3}$ for coordinate vectors, by the diagonal form and bilinearity (Inertial frames and inertial charts of the affine Minkowski model, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

[L2]

Causal classification and cone coordinates: $r$ is timelike when $η (r, r) < 0$ , spacelike when $η (r, r) > 0$ ; in a frame with future first vector, $r$ is future timelike exactly when $r^{0} > ∣ r_{s} ∣$ and past timelike exactly when $r^{0} < - ∣ r_{s} ∣$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones, The timelike set has exactly two convex components, described in orthonormal coordinates).

[L3]

Worldlines (Curves, regular causal curves and future timelike worldlines in affine Minkowski space): a future timelike worldline is a $C^{1}$ curve all of whose tangents are future timelike; the parametrization is part of the curve, and the image of a future timelike worldline is also the image of the past-directed curve $s \mapsto x (- s)$ , which is not a worldline of the model.

[L4]

Constant-integrand evaluation (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ): for a real constant $K$ and $a < b$ , the Riemann integral is $\int_{a}^{b} K = K (b - a)$ . For any timelike $w$ the number $K = \sqrt{- η (w, w)}$ is real; this computation uses no future-orientation or clock-reading premise.

[L5]

Square roots (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Ordered field): $\sqrt{16} = 4$ , and $4 > 0$ .

[L6]

The endpoint bound and its equality case (The endpoint bound for proper time and the maximality of the straight worldline in affine Minkowski space): for a weak piecewise $C^{1}$ future timelike worldline from $p$ to $q$ , $c Δ τ \leq \sqrt{- η (q - p, q - p)}$ with equality exactly for the strictly increasing reparametrizations of the straight segment; the theorem is stated for future timelike worldlines and attaches no reading to past-directed curves.

Counterexample

technique · direct

1.1givenL1L2L5algebra

By [L1], $η (d, d) = - 25 + 9 = - 16 < 0$ and $η (- d, - d) = - 16 < 0$ , while $d^{0} = 5 > 3 = ∣ d_{s} ∣$ and $(- d)^{0} = - 5 < - 3 = - ∣ (- d)_{s} ∣$ ; by [L2] $d$ is future timelike and $- d$ is past timelike, so $\sqrt{- η (d, d)} = \sqrt{16} = 4$ by [L5] and $q - p = - d$ .

2.1step 1.1L3

The curve $x (s) = p - s d$ is $C^{1}$ (indeed affine) on $[0, 1]$ with $x (0) = p$ and $x (1) = p - d = q$ ; its constant tangent is $x^{'} (s) = - d$ , which is nonzero and timelike but past-directed at every $s$ , so by [L3] $x$ is not a future timelike worldline of the model, although it satisfies the 'piecewise $C^{1}$ with nonzero timelike tangents from $p$ to $q$ ' hypothesis of the refuted claim.

3.1step 1.1step 2.1L4algebra

Its length integral is $\int_{0}^{1} \sqrt{- η (- d, - d)} d s = \sqrt{- η (- d, - d)} = 4$ by [L4] and step 1.1, and the endpoint bound is $\sqrt{- η (q - p, q - p)} = \sqrt{- η (- d, - d)} = 4$ ; hence the length integral equals the endpoint bound, with equality.

4.1step 2.1step 3.1L3L6∎

The witness therefore refutes the claim: the length bound can be attained with equality by a past-directed parametrization with no future timelike tangent, so attainment of the bound does not force the future time orientation. This does not contradict [L6], which is stated for future timelike worldlines and whose equality case characterizes the strictly increasing reparametrizations within that class; it distinguishes a numerical length equality from the additional future-orientation convention of the model's worldlines and clock readings.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Worked simultaneity gap of the traveler's two momentary rest frames at the turn

Example

Fix reals $c > 0$ , $T > 0$ , $v = 3 c / 5$ and $γ = 5 / 4$ . This is a mathematical proper-time computation: the inertial chart $x$ has metric $diag (- 1, 1, 1, 1)$ and $x^{0} = c t$ ; the stay-at-home worldline is $y_{s t a y} (t) = x^{- 1} (c t, 0, 0, 0)$ for $t \in [0, 2 T]$ ; the traveler is $y_{t r a v e l} (t) = x^{- 1} (c t, v t, 0, 0)$ on $[0, T]$ and $y_{t r a v e l} (t) = x^{- 1} (c t, v (2 T - t), 0, 0)$ on $[T, 2 T]$ . All clock readings below mean the based mathematical proper-time values of these curves, initialized to zero at $t = 0$ (Proper time along a future timelike worldline, Total proper time of a piecewise C^1 future timelike worldline), so the stay-at-home reading equals $t$ ; the turn event is $r : = x^{- 1} (c T, 3 c T / 5, 0, 0)$ ; the two momentary inertial rest frames of the traveler are the charts $x^{'}$ and $x^{''}$ of the boosts with velocities $+ 3 c / 5$ and $- 3 c / 5$ , both with the same origin $p = x^{- 1} (0, 0, 0, 0)$ as $x$ . Explicitly their bases are $e_{a}^{'} = B (- \frac{3}{5} e_{1}) e_{a}$ and $e_{a}^{''} = B (\frac{3}{5} e_{1}) e_{a}$ for $a = 0, 1, 2, 3$ ; the two charts are defined from these bases and origin by Inertial frames and inertial charts of the affine Minkowski model.

(a) Outbound rest frame. The chart $x^{'}$ has $x^{' 0} = \frac{5}{4} (x^{0} - \frac{3}{5} x^{1})$ ; at $r$ this is $\frac{5}{4} (c T - \frac{3}{5} \cdot \frac{3 c T}{5}) = \frac{5}{4} (c T - \frac{9 c T}{25}) = \frac{5}{4} \cdot \frac{16 c T}{25} = \frac{4 c T}{5}$ , so the slice $x^{' 0} = \frac{4 c T}{5}$ through $r$ meets the stay-at-home worldline $x^{1} = 0$ at $\frac{5}{4} x^{0} = \frac{4 c T}{5}$ , that is $x^{0} = \frac{16 c T}{25}$ , i.e. coordinate time $t = \frac{16 T}{25} = T (1 - \frac{9}{25})$ .

(b) Inbound rest frame. The chart $x^{''}$ has $x^{'' 0} = \frac{5}{4} (x^{0} + \frac{3}{5} x^{1})$ ; at $r$ this is $\frac{5}{4} (c T + \frac{9 c T}{25}) = \frac{5}{4} \cdot \frac{34 c T}{25} = \frac{17 c T}{10}$ , so the slice $x^{'' 0} = \frac{17 c T}{10}$ through $r$ meets the stay-at-home worldline at $\frac{5}{4} x^{0} = \frac{17 c T}{10}$ , that is $x^{0} = \frac{34 c T}{25}$ , i.e. coordinate time $t = \frac{34 T}{25} = T (1 + \frac{9}{25})$ .

(c) The gap. The two momentary frames assign to the stay-at-home clock 'at the time of the turn' the two different readings $\frac{16 T}{25}$ and $\frac{34 T}{25}$ ; their difference is $\frac{18 T}{25} = \frac{2 T v^{2}}{c^{2}}$ , the simultaneity gap.

(d) Reconciliation. The traveler's own clock reads $\frac{4}{5} T = \frac{20 T}{25}$ at the turn and $\frac{8}{5} T = \frac{40 T}{25}$ at the reunion; during each leg his momentary frame assigns to the stay-at-home clock the advance $\frac{16 T}{25}$ (outbound from $0$ to $\frac{16 T}{25}$ ; inbound from $\frac{34 T}{25}$ to $2 T = \frac{50 T}{25}$ ); with the gap $\frac{18 T}{25}$ the total assignment is $\frac{16 T}{25} + \frac{18 T}{25} + \frac{16 T}{25} = \frac{50 T}{25} = 2 T$ , the stay-at-home reading at the reunion, while the traveler reads $\frac{8}{5} T = \frac{40 T}{25}$ ; the two readings differ by $\frac{2 T}{5} = \frac{10 T}{25}$ .

(e) The two rest frames are distinct. Their relative boost parameter is the collinear composition $\frac{2 \cdot (3 / 5)}{1 + 9 / 25} = \frac{6 / 5}{34 / 25} = \frac{15}{17} \neq 0$ , so the traveler's momentary inertial frame changes at the turn.

Facts & Assumptions

Given: An inertial frame with chart $x$ , metric $diag (- 1, 1, 1, 1)$ and $x^{0} = c t$ ; $T > 0$ , $v = 3 c / 5$ , $γ = 5 / 4$ ; the two explicitly parametrized worldlines and mathematical proper-time readings of the Example, the turn event $r = x^{- 1} (c T, 3 c T / 5, 0, 0)$ , the reunion event $q = x^{- 1} (2 c T, 0, 0, 0)$ , and the boost charts $x^{'}$ , $x^{''}$ of the lemma Coordinate formulas of a boost: clock rates, rod lengths, simultaneity and velocity transformation for velocities $+ 3 c / 5$ and $- 3 c / 5$ , both with origin $p = x^{- 1} (0, 0, 0, 0)$ .

[L1]

Boost chart transitions (Coordinate formulas of a boost: clock rates, rod lengths, simultaneity and velocity transformation): for inertial frames with a common origin whose bases are related by a boost of velocity $v$ with $∣ v ∣ < c$ along a common spatial direction one has $x^{' 0} = γ (x^{0} - \frac{v}{c} x^{1})$ , $x^{' 1} = γ (x^{1} - \frac{v}{c} x^{0})$ with $γ = (1 - v^{2} / c^{2})^{- 1 / 2}$ ; and along the worldline at rest in $x^{'}$ the clock rate is $d τ / d t = 1 / γ$ .

[L2]

Simultaneity slices (Simultaneity slices and rest distance relative to a future unit timelike vector, Inertial frames and inertial charts of the affine Minkowski model): for a future unit timelike vector $n$ the slice through an event $p$ is ${u : η (n, u - p) = 0}$ ; in a chart the slice of constant $x^{' 0}$ through an event consists of the events with that coordinate, and coordinate differences of events are the coordinates of their displacements.

[L3]

Boosts (The passive Lorentz boost with parameter beta, The passive boost is a proper orthochronous Lorentz map with inverse B(-beta), Linear and affine Lorentz maps, and the Lorentz group): for $∣ β ∣ < 1$ the passive boost $B (β e)$ is a proper orthochronous Lorentz map, so it maps inertial bases to inertial bases and its charts are inertial charts.

[L4]

Collinear composition (Collinear boost composition and the relativistic velocity-addition law): $B (β_{1} e) B (β_{2} e) = B (\frac{β_{1} + β_{2}}{1 + β_{1} β_{2}} e)$ .

[L5]

Proper times (Proper time along a future timelike worldline, Total proper time of a piecewise C^1 future timelike worldline): a straight leg with constant tangent $(c, \pm v, 0, 0)$ over a parameter interval of length $T$ has proper time $T / γ$ , and the two-leg total is $2 T / γ$ ; the stay-at-home worldline has tangent $(c, 0, 0, 0)$ , so its based proper time is $c^{- 1} \int_{0}^{t} c d u = t$ . This identifies the mathematical reading, without any physical-clock assumption.

[L6]

Arithmetic, roots and order (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Squaring is monotone on the nonnegatives, Ordered field): all the rational evaluations below are exact; $(5 / 4)^{- 1} = 4 / 5$ and $(3 / 5)^{2} = 9 / 25$ .

Verification

technique · direct

1.1givenL1L3L5

By [L1] with $v / c = 3 / 5$ and $γ = 5 / 4$ the outbound chart is $x^{' 0} = \frac{5}{4} (x^{0} - \frac{3}{5} x^{1})$ and the inbound chart is $x^{'' 0} = \frac{5}{4} (x^{0} + \frac{3}{5} x^{1})$ ; both are inertial charts by [L3], and the stay-at-home worldline has $x^{1} = 0$ with clock reading the coordinate time $t = x^{0} / c$ by [L5].

2.1step 1.1L2L6algebra

For (a): the turn event has $x^{0} (r) = c T$ and $x^{1} (r) = 3 c T / 5$ , so $x^{' 0} (r) = \frac{5}{4} (c T - \frac{3}{5} \cdot \frac{3 c T}{5}) = \frac{5}{4} \cdot \frac{16 c T}{25} = \frac{4 c T}{5}$ ; the slice $x^{' 0} = \frac{4 c T}{5}$ meets $x^{1} = 0$ at $\frac{5}{4} x^{0} = \frac{4 c T}{5}$ , that is $x^{0} = \frac{16 c T}{25}$ and clock reading $t = \frac{16 T}{25}$ .

2.2step 1.1L2L6algebra

For (b): $x^{'' 0} (r) = \frac{5}{4} (c T + \frac{3}{5} \cdot \frac{3 c T}{5}) = \frac{5}{4} \cdot \frac{34 c T}{25} = \frac{17 c T}{10}$ ; the slice $x^{'' 0} = \frac{17 c T}{10}$ meets $x^{1} = 0$ at $\frac{5}{4} x^{0} = \frac{17 c T}{10}$ , that is $x^{0} = \frac{34 c T}{25}$ and clock reading $t = \frac{34 T}{25}$ .

2.3step 1.1L4L6algebra

For (e): the outbound frame is obtained from $x$ by a boost of dimensionless parameter $3 / 5$ and the inbound frame by one of parameter $- 3 / 5$ ; the boost from the inbound to the outbound momentary frame is therefore the collinear composition of parameters $3 / 5$ and $3 / 5$ in the composed description, whose parameter is $\frac{3 / 5 + 3 / 5}{1 + (3 / 5) (3 / 5)} = \frac{6 / 5}{34 / 25} = \frac{15}{17}$ by [L4]; since $\frac{15}{17} \neq 0$ , the two momentary inertial frames are distinct.

3.1step 2.1step 2.2L6algebra

For (c): the two readings differ by $\frac{34 T}{25} - \frac{16 T}{25} = \frac{18 T}{25}$ , and $\frac{2 T v^{2}}{c^{2}} = 2 T \cdot \frac{9}{25} = \frac{18 T}{25}$ , so the gap equals $\frac{2 T v^{2}}{c^{2}}$ .

4.1step 3.1L1L5algebra

For (d): by [L5] the traveler's clock reads $T / γ = \frac{4}{5} T = \frac{20 T}{25}$ at the turn and $2 T / γ = \frac{8}{5} T = \frac{40 T}{25}$ at the reunion; the outbound frame assigns to the stay-at-home clock the advance from $t = 0$ to $t = \frac{16 T}{25}$ , namely $\frac{16 T}{25}$ , the inbound frame assigns the advance from $t = \frac{34 T}{25}$ to $t = 2 T = \frac{50 T}{25}$ , again $\frac{16 T}{25}$ , so with the gap the total assigned reading is $\frac{16 T}{25} + \frac{18 T}{25} + \frac{16 T}{25} = \frac{50 T}{25} = 2 T$ , equal to the stay-at-home clock reading at the reunion, while the traveler reads $\frac{40 T}{25}$ ; the readings differ by $\frac{10 T}{25} = \frac{2 T}{5}$ .

5.1step 2.1step 2.2step 3.1step 4.1step 2.3L1L2L4L5∎

All the numbers of (a)-(e) are exact rational evaluations of the model's chart transitions, slices and proper-time values: the simultaneity gap of the traveler's two momentary frames at the turn is $\frac{18 T}{25} = \frac{2 T v^{2}}{c^{2}}$ , and the leg-by-leg assignment $\frac{16 T}{25} + \frac{18 T}{25} + \frac{16 T}{25} = 2 T$ reproduces the stay-at-home reading. The example makes no empirical claim; it displays a reconciliation of the traveler's momentary-frame accounts within the model.

Proper Time Comparisons — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

5 · Examples, experiments and counterexamples

Worked reverse Cauchy-Schwarz and reverse triangle inequalities

Example

Facts & Assumptions

Verification

Counterexample: the reversed Cauchy-Schwarz inequality fails outside same-orientation timelike pairs

Statement refuted

Facts & Assumptions

Counterexample

Worked rest frame of the future timelike displacement (5,3,0,0)

Example

Facts & Assumptions

Verification

Worked two-leg itinerary against the straight clock at speed 3c/5

Example

Facts & Assumptions

Verification

Counterexample: attainment of the endpoint bound does not force the future time orientation

Statement refuted

Facts & Assumptions

Counterexample

Worked simultaneity gap of the traveler's two momentary rest frames at the turn

Example

Facts & Assumptions

Verification

Sources