Orthogonal decomposition relative to a timelike vector

This file develops the infrastructure needed for the sign lemma for cones: two timelike vectors that are future-pointing with respect to a common time orientation have negative inner product.

For a symmetric Lorentzian bilinear form B and a timelike vector t (B t t < 0), the orthogonal complement t^⊥ = {u | B t u = 0} is the spacelike complement. The two key facts are:

• nonneg_of_orthogonal_timelike: B is positive semidefinite on t^⊥ (it would be positive definite under nondegeneracy, but semidefiniteness is all that the sign lemma needs and it follows directly from reverse Cauchy-Schwarz);
• cauchy_schwarz_on_orthogonal: the ordinary (forward) Cauchy-Schwarz inequality holds for vectors in t^⊥.

Combining these with the explicit t-orthogonal decomposition (B t t) • v - (B t v) • t ∈ t^⊥ yields bilin_neg_of_inner_t_neg, the sign lemma.

All statements are abstract (they depend only on the algebraic LorentzianAt condition), so they transfer to the metric g|_p of any spacetime.

theorem Physicslib4.inner_orthogonal_component {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (t v : V) : (B t) ((B t) t • v - (B t) v • t) = 0

The t-orthogonal component of v, cleared of denominators by the factor B t t: the vector (B t t) • v - (B t v) • t is orthogonal to t.

theorem Physicslib4.nonneg_of_orthogonal_timelike {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) {t u : V} (ht : (B t) t < 0) (h : (B t) u = 0) : 0 ≤ (B u) u

Positive semidefiniteness of the spacelike complement. If t is timelike and u is orthogonal to t, then 0 ≤ B u u: were B u u < 0, the vector u would be timelike and reverse Cauchy-Schwarz would force (B t u)^2 > 0, contradicting orthogonality.

theorem Physicslib4.cauchy_schwarz_of_nonneg_on_span {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hsymm : ∀ (v w : V), (B v) w = (B w) v) {x y : V} (h : ∀ (s : ℝ), 0 ≤ (B (s • x + y)) (s • x + y)) : (B x) y ^ 2 ≤ (B x) x * (B y) y

Cauchy-Schwarz for two vectors along whose span the symmetric form B is positive semidefinite. Proved via the nonpositivity of the discriminant of the nonnegative quadratic s ↦ B (s • x + y) (s • x + y).

theorem Physicslib4.cauchy_schwarz_on_orthogonal {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) {t x y : V} (ht : (B t) t < 0) (hx : (B t) x = 0) (hy : (B t) y = 0) : (B x) y ^ 2 ≤ (B x) x * (B y) y

Forward Cauchy-Schwarz on the spacelike complement. For two vectors orthogonal to a timelike vector t, the ordinary Cauchy-Schwarz inequality holds.

theorem Physicslib4.eq_zero_of_forall_bilin_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] {B : LinearMap.BilinForm ℝ V} (hL : LorentzianAt fun (v w : V) => (B v) w) {v : V} (h : ∀ (w : V), (B v) w = 0) : v = 0

Nondegeneracy from the Lorentzian basis. A Lorentzian bilinear form is nondegenerate: if B v w = 0 for every w, then v = 0. This is extracted from the signature basis, on which the Gram matrix diag(-1,1,1,1) is invertible.

theorem Physicslib4.pos_of_orthogonal_timelike {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) {t u : V} (ht : (B t) t < 0) (h : (B t) u = 0) (hu : u ≠ 0) : 0 < (B u) u

Strict positive-definiteness of the spacelike complement. If t is timelike and u ≠ 0 is orthogonal to t, then 0 < B u u. A null vector in t^⊥ would, by Cauchy-Schwarz on t^⊥, be orthogonal to all of t^⊥, hence to everything, contradicting nondegeneracy.

theorem Physicslib4.bilin_neg_of_inner_t_neg {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) {t v w : V} (ht : (B t) t < 0) (hv : (B v) v < 0) (hw : (B w) w < 0) (htv : (B t) v < 0) (htw : (B t) w < 0) : (B v) w < 0

Sign lemma for cones. Let B be a symmetric Lorentzian bilinear form, t a timelike vector, and v, w timelike vectors that are future-pointing with respect to t (B t v < 0 and B t w < 0). Then B v w < 0: future-pointing timelike vectors lie in a common cone, on which the inner product is negative.

theorem Physicslib4.Spacetime.inner_neg_of_future_timelike (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v w : TangentSpace M.model x} (hv : M.IsTimelike v) (hw : M.IsTimelike w) (hfv : ((M.val x) (τ.field x)) v < 0) (hfw : ((M.val x) (τ.field x)) w < 0) : ((M.val x) v) w < 0

Spacetime sign lemma. Two timelike tangent vectors at a point that are future-pointing with respect to the same time orientation τ (g|_p(τ,v) < 0 and g|_p(τ,w) < 0) have negative inner product g|_p(v,w) < 0.

theorem Physicslib4.Spacetime.isSpacelike_of_orthogonal_timelike (M : Spacetime) (x : M.Carrier) {t u : TangentSpace M.model x} (ht : M.IsTimelike t) (h : ((M.val x) t) u = 0) (hu : u ≠ 0) : M.IsSpacelike u

Spacelike complement, pointwise. A nonzero tangent vector orthogonal to a timelike vector is spacelike: the metric is positive definite on the spacelike complement.

theorem Physicslib4.Spacetime.isFuturePointing_add (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v w : TangentSpace M.model x} (hv : M.IsTimelike v) (hw : M.IsTimelike w) (hfv : M.IsFuturePointing τ v) (hfw : M.IsFuturePointing τ w) : M.IsFuturePointing τ (v + w)

Convexity of the future cone (timelike part). The sum of two timelike future-pointing tangent vectors is again timelike and future-pointing with respect to the same time orientation. This is the cone-convexity payoff of the sign lemma.

theorem Physicslib4.Spacetime.exists_seq_of_isFuturePointing (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v : TangentSpace M.model x} (hv : M.IsFuturePointing τ v) : ∃ (vs : ℕ → TangentSpace M.model x), (∀ (n : ℕ), M.IsTimelike (vs n) ∧ ((M.val x) (τ.field x)) (vs n) < 0) ∧ Filter.Tendsto vs Filter.atTop (nhds v)

Every future-pointing vector (timelike or null) is the limit of a sequence of future-pointing timelike vectors. For a timelike vector this is the constant sequence; for a null vector it is exactly the approximating sequence in the definition of IsFuturePointing.

theorem Physicslib4.Spacetime.inner_t_nonpos_of_future (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v : TangentSpace M.model x} (hfv : M.IsFuturePointing τ v) : ((M.val x) (τ.field x)) v ≤ 0

The time-orientation pairing is nonpositive on any future-pointing vector: g|_p(τ, v) ≤ 0. For timelike v this is the defining strict inequality; for null v it follows by passing to the limit along the approximating sequence (continuity of the fixed continuous linear functional g|_p(τ, ·)).

theorem Physicslib4.Spacetime.inner_nonpos_of_future (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v w : TangentSpace M.model x} (hfv : M.IsFuturePointing τ v) (hfw : M.IsFuturePointing τ w) : ((M.val x) v) w ≤ 0

Generalized sign lemma. Any two future-pointing vectors (timelike or null) have nonpositive inner product g|_p(v,w) ≤ 0. Only continuity of the fixed continuous linear maps g|_p(a, ·) is used (with symmetry to keep the varying vector in the second slot), so no normed structure on the tangent space is required.

theorem Physicslib4.Spacetime.isFuturePointing_add_general (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v w : TangentSpace M.model x} (hfv : M.IsFuturePointing τ v) (hfw : M.IsFuturePointing τ w) : M.IsFuturePointing τ (v + w)

Convexity of the future cone (general form). The sum of any two future-pointing tangent vectors (timelike or null) is future-pointing with respect to the same time orientation. The timelike summands are handled by isFuturePointing_add; the null branch is treated by approximating each summand by future-pointing timelike vectors and passing to the limit.

theorem Physicslib4.Spacetime.isPastPointing_iff_isFuturePointing_neg (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v : TangentSpace M.model x} : M.IsPastPointing τ v ↔ M.IsFuturePointing τ (-v)

Time reversal. A tangent vector is past-pointing with respect to a time orientation exactly when its negation is future-pointing.

theorem Physicslib4.Spacetime.inner_neg_of_past_timelike (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v w : TangentSpace M.model x} (hv : M.IsTimelike v) (hw : M.IsTimelike w) (hpv : 0 < ((M.val x) (τ.field x)) v) (hpw : 0 < ((M.val x) (τ.field x)) w) : ((M.val x) v) w < 0

Past-cone sign lemma. Two timelike tangent vectors that are past-pointing with respect to the same time orientation have negative inner product. (Time reversal of inner_neg_of_future_timelike.)

theorem Physicslib4.Spacetime.isPastPointing_add (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v w : TangentSpace M.model x} (hfv : M.IsPastPointing τ v) (hfw : M.IsPastPointing τ w) : M.IsPastPointing τ (v + w)

Convexity of the past cone. The sum of any two past-pointing tangent vectors (timelike or null) is past-pointing. Obtained from isFuturePointing_add_general by time reversal.

theorem Physicslib4.Spacetime.isFuturePointing_smul_pos (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v : TangentSpace M.model x} {c : ℝ} (hc : 0 < c) (hfv : M.IsFuturePointing τ v) : M.IsFuturePointing τ (c • v)

Positive scaling preserves future-pointing. A positive multiple of a future-pointing vector is future-pointing.

theorem Physicslib4.Spacetime.isFuturePointing_pos_combination (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v w : TangentSpace M.model x} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hfv : M.IsFuturePointing τ v) (hfw : M.IsFuturePointing τ w) : M.IsFuturePointing τ (a • v + b • w)

The future cone is a convex cone. Any positive linear combination of two future-pointing tangent vectors is future-pointing. This is the convex-cone packaging of isFuturePointing_add_general, the downstream form of cone convexity consumed elsewhere in the causal structure.

theorem Physicslib4.Spacetime.isPastPointing_smul_pos (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v : TangentSpace M.model x} {c : ℝ} (hc : 0 < c) (hfv : M.IsPastPointing τ v) : M.IsPastPointing τ (c • v)

Positive scaling preserves past-pointing (time reversal of isFuturePointing_smul_pos).

theorem Physicslib4.Spacetime.isPastPointing_pos_combination (M : Spacetime) (x : M.Carrier) (τ : M.TimeOrientation) {v w : TangentSpace M.model x} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hfv : M.IsPastPointing τ v) (hfw : M.IsPastPointing τ w) : M.IsPastPointing τ (a • v + b • w)

The past cone is a convex cone. Any positive linear combination of two past-pointing tangent vectors is past-pointing.