LemmaStatement: 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.

The reversed Cauchy-Schwarz inequality for future timelike vectors

Statement

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski space and let $v, w \in V$ be future timelike vectors. Put $a : = \sqrt{- η (v, v)} > 0$ and $b : = \sqrt{- η (w, w)} > 0$ , the timelike lengths of $v$ and $w$ . Then:

(i) $- η (v, w) \geq a b > 0$ .

(ii) Equality $- η (v, w) = a b$ holds if and only if $v$ and $w$ are positive proportional, that is $w = t v$ for some real $t > 0$ , or $v = t w$ for some real $t > 0$ .

(iii) Consequently $- η (v, w) > a b$ whenever $v$ and $w$ are not positive proportional, and $η (v, w) < 0$ in every case.

(iv) For two past timelike vectors $v, w$ the same inequality $- η (v, w) \geq \sqrt{- η (v, v)} \sqrt{- η (w, w)}$ holds, with equality if and only if they are positive proportional, because $- v$ and $- w$ are future timelike and $η (- v, - w) = η (v, w)$ .

The statement uses only $η$ and the future cone $C^{+}$ and involves no chart, frame or choice principle.

Facts & Assumptions

Given: The oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ and future timelike vectors $v, w \in V$ , with $a : = \sqrt{- η (v, v)} > 0$ and $b : = \sqrt{- η (w, w)} > 0$ .

[F1]

Inertial frames and charts: at every event $o \in A$ there is an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ ; its ordered basis is $η$ -orthonormal with $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ , its first vector $e_{0}$ lies in $C^{+}$ , and $E (u) : = \sum_{a} u^{a} e_{a}$ is a linear isomorphism $E : R^{4} \to V$ , so every vector $u \in V$ has unique coordinates $u = u^{0} e_{0} + u_{s}$ with $u_{s} = u^{1} e_{1} + u^{2} e_{2} + u^{3} e_{3}$ (Existence of future-oriented inertial frames at every event, Inertial frames and inertial charts of the affine Minkowski model).

[F2]

Cone coordinates: in an $η$ -orthonormal basis whose first vector is timelike the timelike set is the disjoint union $T = T_{+} \cup T_{-}$ with $T_{+} = {u : u^{0} > ∣ u_{s} ∣}$ and $T_{-} = {u : u^{0} < - ∣ u_{s} ∣}$ , and $T_{+}$ , $T_{-}$ are exactly the two connected components of $T$ ; the time orientation selects one component $C^{+}$ and $C^{-} : = T ∖ C^{+}$ is the other, so with the basis of [F1], where $e_{0} \in C^{+}$ , one has $C^{+} = T_{+}$ and $C^{-} = T_{-} = - C^{+}$ ; hence $u$ is future timelike if and only if $u^{0} > ∣ u_{s} ∣$ , and $u$ is past timelike if and only if $- u$ is future timelike (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).

[F3]

Spatial and bilinear structure: for a frame of [F1], the spatial three-space $S : = span (e_{1}, e_{2}, e_{3}) = {z \in V : η (e_{0}, z) = 0}$ carries the restriction $δ : = η ∣_{S}$ , which is positive definite, and $∣ z ∣ : = \sqrt{δ (z, z)}$ is a norm on $S$ with $(e_{1}, e_{2}, e_{3})$ a $δ$ -orthonormal basis; since $η$ is bilinear, for all $u = u^{0} e_{0} + u_{s}$ and $u^{'} = u^{' 0} e_{0} + u_{s}^{'}$ one has $η (u, u^{'}) = - u^{0} u^{' 0} + δ (u_{s}, u_{s}^{'})$ , and in particular $η (u, u) = - (u^{0})^{2} + ∣ u_{s} ∣^{2}$ (The Euclidean spatial structure and cross product of an inertial frame, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

[L4]

Finite Cauchy-Schwarz inequality: for reals $a_{0}, \dots, a_{n - 1}$ and $b_{0}, \dots, b_{n - 1}$ one has $(\sum_{k < n} a_{k} b_{k})^{2} \leq (\sum_{k < n} a_{k}^{2}) (\sum_{k < n} b_{k}^{2})$ and $∣ \sum_{k < n} a_{k} b_{k} ∣ \leq \sqrt{\sum_{k < n} a_{k}^{2}} \sqrt{\sum_{k < n} b_{k}^{2}}$ ; equality holds in the first display if and only if the two lists are proportional in the sense that there is a pair $(λ, μ) \neq (0, 0)$ of reals with $λ a_{k} = μ b_{k}$ for every $k < n$ (The Cauchy-Schwarz inequality for finite sums).

[L5]

Square roots and monotonicity of squaring: every real $c \geq 0$ has a unique $\sqrt{c} \geq 0$ with $(\sqrt{c})^{2} = c$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ); for $x, y \geq 0$ one has $x \leq y ⟺ x^{2} \leq y^{2}$ and $x < y ⟺ x^{2} < y^{2}$ (Squaring is monotone on the nonnegatives); for $c > 0$ the root notation is the rational power $c^{1 / 2}$ (Rational powers $a^{r}$ of a positive base).

[L6]

Order arithmetic of $R$ : a product of two positive reals is positive and a product of a positive and a negative real is negative (Sign rules for products and monotonicity of multiplication); inequalities may be added, and a constant may be added to both sides of an inequality (Order is preserved by adding a constant and by adding inequalities); and for reals $x, y$ exactly one of $x < y$ , $x = y$ , $x > y$ holds, a product of reals vanishes only if a factor vanishes, and $x \geq 0$ means $x > 0$ or $x = 0$ (Ordered field).

Proof

technique · direct

1.1givenF1F3choose

Fix an event $o \in A$ and an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with its basis and chart, and write $v = v^{0} e_{0} + v_{s}$ , $w = w^{0} e_{0} + w_{s}$ with spatial parts $v_{s}, w_{s} \in S$ ; the coordinates are unique by [F1] and the spatial parts lie in $S$ by the definition of $S$ in [F3].

2.1step 1.1F2F3L5L6

Since $v$ and $w$ are future timelike, [F2] gives $v^{0} > ∣ v_{s} ∣$ and $w^{0} > ∣ w_{s} ∣$ ; as $∣ v_{s} ∣, ∣ w_{s} ∣ \geq 0$ by [F3], this yields $v^{0} > 0$ , $w^{0} > 0$ , and by strict monotonicity of squaring on the nonnegatives $(v^{0})^{2} > ∣ v_{s} ∣^{2}$ and $(w^{0})^{2} > ∣ w_{s} ∣^{2}$ , so $a^{2} = (v^{0})^{2} - ∣ v_{s} ∣^{2} > 0$ and $b^{2} = (w^{0})^{2} - ∣ w_{s} ∣^{2} > 0$ , whence $a = \sqrt{(v^{0})^{2} - ∣ v_{s} ∣^{2}} > 0$ and $b = \sqrt{(w^{0})^{2} - ∣ w_{s} ∣^{2}} > 0$ by uniqueness of the nonnegative root.

2.2step 1.1F3L4algebra

By bilinearity [F3], $- η (v, w) = v^{0} w^{0} - δ (v_{s}, w_{s})$ ; applying the finite Cauchy-Schwarz inequality [L4] to the coordinates of $v_{s}$ and $w_{s}$ in the $δ$ -orthonormal basis $(e_{1}, e_{2}, e_{3})$ gives $∣ δ (v_{s}, w_{s}) ∣ \leq ∣ v_{s} ∣ ∣ w_{s} ∣$ , hence $δ (v_{s}, w_{s}) \leq ∣ v_{s} ∣ ∣ w_{s} ∣$ and $- η (v, w) \geq x$ for $x : = v^{0} w^{0} - ∣ v_{s} ∣ ∣ w_{s} ∣$ .

3.1step 2.1L6algebra

The algebraic identity $x^{2} - ((v^{0})^{2} - ∣ v_{s} ∣^{2}) ((w^{0})^{2} - ∣ w_{s} ∣^{2}) = (v^{0} ∣ w_{s} ∣ - w^{0} ∣ v_{s} ∣)^{2} \geq 0$ holds by expansion, so $x^{2} \geq a^{2} b^{2}$ ; moreover $x = w^{0} (v^{0} - ∣ v_{s} ∣) + ∣ v_{s} ∣ (w^{0} - ∣ w_{s} ∣)$ is a sum of a positive real and a nonnegative real, so $x > 0$ and in particular $x \geq 0$ .

4.1step 2.1step 2.2step 3.1L5L6

Since $x \geq 0$ and $a b > 0$ with $x^{2} \geq (a b)^{2}$ , monotonicity of squaring on the nonnegatives [L5] gives $x \geq a b$ , and with step 2.2 this yields $- η (v, w) \geq a b > 0$ , which is (i); equivalently $η (v, w) \leq - a b < 0$ .

5.1step 2.2step 3.1step 4.1algebra

Assume now $- η (v, w) = a b$ . Then the chain $a b = - η (v, w) \geq x \geq a b$ of steps 2.2 and 4.1 is equality at both places, so $δ (v_{s}, w_{s}) = ∣ v_{s} ∣ ∣ w_{s} ∣$ , and from $x = a b$ and the identity of step 3.1 we get $(v^{0} ∣ w_{s} ∣ - w^{0} ∣ v_{s} ∣)^{2} = x^{2} - (a b)^{2} = 0$ , that is $v^{0} ∣ w_{s} ∣ = w^{0} ∣ v_{s} ∣$ .

6.1step 2.1step 5.1L6

Case $v_{s} = 0$ : then $v^{0} ∣ w_{s} ∣ = w^{0} ∣ v_{s} ∣ = 0$ by step 5.1, and $v^{0} > 0$ , so $∣ w_{s} ∣ = 0$ and hence $w_{s} = 0$ ; therefore $v = v^{0} e_{0}$ and $w = w^{0} e_{0}$ with $v^{0}, w^{0} > 0$ , and $v = (v^{0} / w^{0}) w$ exhibits $v$ as a positive multiple of $w$ .

6.2step 2.1step 5.1L6

Case $w_{s} = 0$ : symmetrically $w^{0} ∣ v_{s} ∣ = v^{0} ∣ w_{s} ∣ = 0$ with $w^{0} > 0$ gives $v_{s} = 0$ , and $v^{0} > 0$ gives $w = (w^{0} / v^{0}) v$ , so $w$ is a positive multiple of $v$ .

6.3step 5.1L4L5L6algebra

Case $v_{s} \neq 0$ and $w_{s} \neq 0$ : the equality $δ (v_{s}, w_{s}) = ∣ v_{s} ∣ ∣ w_{s} ∣ > 0$ of step 5.1 is the equality case of the finite Cauchy-Schwarz inequality [L4] for two nonzero lists, so there are reals $(λ, μ) \neq (0, 0)$ with $λ v_{s} = μ w_{s}$ ; here $λ \neq 0$ (otherwise $w_{s} = 0$ ) and $μ \neq 0$ (otherwise $v_{s} = 0$ ), so $v_{s} = c w_{s}$ with $c : = μ / λ$ , and then $δ (v_{s}, w_{s}) = c ∣ w_{s} ∣^{2}$ while $∣ v_{s} ∣ = ∣ c ∣ ∣ w_{s} ∣$ , so $c ∣ w_{s} ∣^{2} = ∣ c ∣ ∣ w_{s} ∣^{2}$ with $∣ w_{s} ∣^{2} = δ (w_{s}, w_{s}) > 0$ ; hence $c = ∣ c ∣ \geq 0$ , and $c > 0$ because $c ∣ w_{s} ∣^{2} = ∣ v_{s} ∣ ∣ w_{s} ∣ > 0$ ; finally $v^{0} ∣ w_{s} ∣ = w^{0} ∣ v_{s} ∣ = w^{0} c ∣ w_{s} ∣$ with $∣ w_{s} ∣ > 0$ gives $v^{0} = c w^{0}$ , so $v = v^{0} e_{0} + c w_{s} = c (w^{0} e_{0} + w_{s}) = c w$ with $c > 0$ .

7.1step 6.1step 6.2step 6.3

The three cases of steps 6.1-6.3 exhaust the possibilities, so equality $- η (v, w) = a b$ forces $v$ and $w$ to be positive proportional; this is the forward implication of (ii).

8.1step 2.1F3L5algebra

Conversely, if $v = t w$ with $t > 0$ , then bilinearity gives $- η (v, w) = - t η (w, w) = t b^{2}$ and $- η (v, v) = - t^{2} η (w, w) = t^{2} b^{2}$ , so $a = t b$ by uniqueness of the nonnegative square root, whence $- η (v, w) = t b \cdot b = a b$ ; the case $w = t v$ is identical, and together with step 7.1 this proves (ii).

9.1step 4.1step 7.1step 8.1

For (iii): if $v$ and $w$ are not positive proportional then equality fails by (ii), so $- η (v, w) > a b$ by step 4.1, while $η (v, w) < 0$ holds in every case again by step 4.1.

10.1step 4.1step 7.1step 8.1F2F3∎

For (iv): if $v, w$ are past timelike then $- v, - w$ are future timelike by [F2], with $- η (- v, - v) = - η (v, v)$ , $- η (- w, - w) = - η (w, w)$ and $η (- v, - w) = η (v, w)$ by bilinearity [F3]; steps 4.1, 7.1 and 8.1 applied to $- v, - w$ therefore give $- η (v, w) = - η (- v, - w) \geq a b$ , with equality exactly when $- v, - w$ are positive proportional, that is exactly when $v, w$ are positive proportional.

The reversed Cauchy-Schwarz inequality for future timelike vectors

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources