Convexity of the timelike cone and the reverse triangle inequality

This file formalises the blueprint declaration lmm:timelike-cone-convexity (Chapter 10, sections/sec10/10-2_spacetime).

For a symmetric Lorentzian bilinear form g (signature diag(-1,1,1,1)) two timelike vectors v, w are aligned (share a time cone) when g v w ≤ 0. For such vectors:

• v + w is again timelike (convexity of the timelike cone), and
• the reverse (Lorentzian) triangle inequality holds: √(-(g v v)) + √(-(g w w)) ≤ √(-(g (v+w) (v+w))).

The closure under addition is elementary; the reverse triangle inequality is the substantive statement and consumes the reverse Cauchy-Schwarz inequality reverse_cauchy_schwarz_of_lorentzianAt (lmm:reverse-cauchy-schwarz).

The abstract lemmas depend only on the algebraic LorentzianAt condition, so they transfer verbatim to the metric g|_p of any spacetime; Spacetime.add_isTimelike and Spacetime.reverse_triangle are the specialisations.

Modelling note

The alignment hypothesis g v w ≤ 0 encodes "v and w lie in the same time cone". For two future-pointing timelike vectors this sign holds, but proving it from the future-pointing condition alone requires the positive-definiteness of the spacelike complement (a signature/inertia argument), which is not available from the pointwise LorentzianAt data; we therefore take the sign as an explicit hypothesis.

theorem Physicslib4.add_isTimelike_of_lorentzianAt {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hsymm : ∀ (v w : V), (B v) w = (B w) v) {v w : V} (hv : (B v) v < 0) (hw : (B w) w < 0) (haligned : (B v) w ≤ 0) : (B (v + w)) (v + w) < 0

Convexity of the timelike cone. The sum of two aligned timelike vectors (g v w ≤ 0) of a symmetric Lorentzian bilinear form is again timelike.

theorem Physicslib4.reverse_triangle_of_lorentzianAt {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hsymm : ∀ (v w : V), (B v) w = (B w) v) (hL : LorentzianAt fun (v w : V) => (B v) w) {v w : V} (hv : (B v) v < 0) (hw : (B w) w < 0) (haligned : (B v) w ≤ 0) : √(-(B v) v) + √(-(B w) w) ≤ √(-(B (v + w)) (v + w))

Reverse (Lorentzian) triangle inequality for two aligned timelike vectors of a symmetric Lorentzian bilinear form. This is where the reverse Cauchy-Schwarz inequality is consumed.

theorem Physicslib4.Spacetime.add_isTimelike (M : Spacetime) (x : M.Carrier) {v w : TangentSpace M.model x} (hv : M.IsTimelike v) (hw : M.IsTimelike w) (haligned : ((M.val x) v) w ≤ 0) : M.IsTimelike (v + w)

Convexity of the timelike cone for the metric of a spacetime: the sum of two aligned timelike tangent vectors (g|_p(v,w) ≤ 0) at a point is timelike.

theorem Physicslib4.Spacetime.reverse_triangle (M : Spacetime) (x : M.Carrier) {v w : TangentSpace M.model x} (hv : M.IsTimelike v) (hw : M.IsTimelike w) (haligned : ((M.val x) v) w ≤ 0) : √(-((M.val x) v) v) + √(-((M.val x) w) w) ≤ √(-((M.val x) (v + w)) (v + w))

Reverse (Lorentzian) triangle inequality for the metric of a spacetime: two aligned timelike tangent vectors at a point satisfy √(-g(v,v)) + √(-g(w,w)) ≤ √(-g(v+w,v+w)).