From 68abc2ecb43a0f61cf61e156bbef49be82f4eeb8 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 10 Sep 2026 21:41:22 +0200 Subject: [PATCH 1/3] feat(Relativity): reverse Cauchy-Schwarz and triangle inequalities, twin paradox age gap nonnegative Adds Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean with IsFutureCausal, isFutureCausal_of_causallyFollows, the elementary inequality sqrt_mul_sqrt_le, norm_spatialPart_le_timeComponent, the reverse Cauchy-Schwarz inequality sqrt_mul_sqrt_le_minkowskiProduct, minkowskiProduct_add_self, the reverse triangle inequality sqrt_add_sqrt_le_sqrt_add and isFutureCausal_add. In Physlib/Relativity/Special/TwinParadox/Basic.lean, replaces the informal lemma ageGap_nonneg (tag 7ROVE) by a proof. Generated with Claude Code under human supervision (see AI-POLICY.md). Co-authored-by: Claude Fable 5.1 --- Physlib.lean | 1 + .../Relativity/Special/TwinParadox/Basic.lean | 18 ++- .../Vector/Causality/ReverseTriangle.lean | 150 ++++++++++++++++++ 3 files changed, 164 insertions(+), 5 deletions(-) create mode 100644 Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean diff --git a/Physlib.lean b/Physlib.lean index 43587e6225..e5dd806bd8 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -469,6 +469,7 @@ public import Physlib.Relativity.Tensors.RealTensor.Units.Pre public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.Basic public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike +public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.ReverseTriangle public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Basic diff --git a/Physlib/Relativity/Special/TwinParadox/Basic.lean b/Physlib/Relativity/Special/TwinParadox/Basic.lean index a5760b0c9f..b02f3ea903 100644 --- a/Physlib/Relativity/Special/TwinParadox/Basic.lean +++ b/Physlib/Relativity/Special/TwinParadox/Basic.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.Special.ProperTime +public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.ReverseTriangle /-! # Twin Paradox @@ -67,11 +68,18 @@ def ageGap : ℝ := T.properTimeTwinA - T.properTimeTwinB TODO "Find the conditions for which the age gap for the twin paradox is zero." -/-- In the twin paradox with instantaneous acceleration, Twin A is always older - then Twin B. -/ -informal_lemma ageGap_nonneg where - deps := [``ageGap] - tag := "7ROVE" +/-- In the twin paradox with instantaneous acceleration, Twin A is always at least as old as + Twin B: the age gap is nonnegative. This is the reverse triangle inequality of Minkowski space + (`sqrt_add_sqrt_le_sqrt_add`) applied to the two legs of Twin B. -/ +lemma ageGap_nonneg : 0 ≤ T.ageGap := by + have hu := isFutureCausal_of_causallyFollows T.twinBMid_causallyFollows_startPoint + have hv := isFutureCausal_of_causallyFollows T.endPoint_causallyFollows_twinBMid + have h := sqrt_add_sqrt_le_sqrt_add hu hv + have hsum : T.endPoint - T.startPoint + = (T.twinBMid - T.startPoint) + (T.endPoint - T.twinBMid) := by abel + unfold ageGap properTimeTwinA properTimeTwinB properTime + rw [hsum] + linarith /-! diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean new file mode 100644 index 0000000000..3a0b8ec405 --- /dev/null +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean @@ -0,0 +1,150 @@ +/- +Copyright (c) 2026 Philippe Kevorkian. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Philippe Kevorkian +-/ +module + +public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike +public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike +/-! + +# The reverse Cauchy-Schwarz and reverse triangle inequalities + +## i. Overview + +For two future-directed causal vectors `u`, `v` of Minkowski space (signature `+---`), the +Minkowski product dominates the product of the Minkowski norms, `⟪u, v⟫ₘ ≥ √⟪u, u⟫ₘ √⟪v, v⟫ₘ` +(reverse Cauchy-Schwarz inequality), and the Minkowski norm of the sum dominates the sum of the +norms, `√⟪u + v, u + v⟫ₘ ≥ √⟪u, u⟫ₘ + √⟪v, v⟫ₘ` (reverse triangle inequality). The proof reduces to +the elementary inequality `√(a² - c²) √(b² - d²) ≤ a b - c d` for `0 ≤ c ≤ a`, `0 ≤ d ≤ b`, applied +to the time components and the Euclidean norms of the spatial parts, together with the Euclidean +Cauchy-Schwarz inequality. + +## ii. Key results + +- `IsFutureCausal`: `0 ≤ ⟪u, u⟫ₘ` and `0 ≤ u⁰`; `isFutureCausal_of_causallyFollows`. +- `sqrt_mul_sqrt_le`: the elementary inequality. +- `norm_spatialPart_le_timeComponent`: `‖u_spatial‖ ≤ u⁰` for `u` future causal. +- `sqrt_mul_sqrt_le_minkowskiProduct`: the reverse Cauchy-Schwarz inequality. +- `sqrt_add_sqrt_le_sqrt_add`: the reverse triangle inequality; `isFutureCausal_add`. + +## iii. Table of contents + +- A. Future-directed causal vectors +- B. The elementary inequality +- C. The reverse Cauchy-Schwarz inequality +- D. The reverse triangle inequality + +-/ + +@[expose] public section + +namespace Lorentz + +namespace Vector + +open InnerProductSpace + +/-! + +## A. Future-directed causal vectors + +-/ + +/-- A vector is future-directed causal if it is time-like or light-like (`0 ≤ ⟪u, u⟫ₘ`) with a + nonnegative time component. -/ +def IsFutureCausal {d : ℕ} (u : Vector d) : Prop := 0 ≤ ⟪u, u⟫ₘ ∧ 0 ≤ u.timeComponent + +/-- The vector from `p` to `q` is future-directed causal when `q` causally follows `p`. -/ +lemma isFutureCausal_of_causallyFollows {d : ℕ} {p q : Vector d} (h : causallyFollows p q) : + IsFutureCausal (q - p) := by + rcases h with h | h + · obtain ⟨h1, h2⟩ := h + exact ⟨((timeLike_iff_norm_sq_pos _).mp h1).le, h2.le⟩ + · obtain ⟨h1, h2⟩ := h + exact ⟨((lightLike_iff_norm_sq_zero _).mp h1).ge, h2⟩ + +/-! + +## B. The elementary inequality + +-/ + +/-- For `0 ≤ c ≤ a` and `0 ≤ d ≤ b`, `√(a² - c²) √(b² - d²) ≤ a b - c d`: indeed + `(a b - c d)² - (a² - c²)(b² - d²) = (a d - b c)²`. -/ +lemma sqrt_mul_sqrt_le {a b c d : ℝ} (hc : 0 ≤ c) (hca : c ≤ a) (hd : 0 ≤ d) (hdb : d ≤ b) : + √(a ^ 2 - c ^ 2) * √(b ^ 2 - d ^ 2) ≤ a * b - c * d := by + have h1 : 0 ≤ a ^ 2 - c ^ 2 := by nlinarith + have h2 : 0 ≤ a * b - c * d := by nlinarith + calc √(a ^ 2 - c ^ 2) * √(b ^ 2 - d ^ 2) = √((a ^ 2 - c ^ 2) * (b ^ 2 - d ^ 2)) := + (Real.sqrt_mul h1 _).symm + _ ≤ √((a * b - c * d) ^ 2) := Real.sqrt_le_sqrt (by nlinarith [sq_nonneg (a * d - b * c)]) + _ = a * b - c * d := Real.sqrt_sq h2 + +/-! + +## C. The reverse Cauchy-Schwarz inequality + +-/ + +/-- `⟪u, u⟫ₘ = (u⁰)² - ‖u_spatial‖²`. -/ +lemma minkowskiProduct_self_eq_sq_sub {d : ℕ} (u : Vector d) : + ⟪u, u⟫ₘ = u.timeComponent ^ 2 - ‖u.spatialPart‖ ^ 2 := by + rw [minkowskiProduct_self_eq_timeComponent_spatialPart, Real.norm_eq_abs, sq_abs] + +/-- For a future-directed causal vector, the Euclidean norm of the spatial part is at most the + time component. -/ +lemma norm_spatialPart_le_timeComponent {d : ℕ} {u : Vector d} (hu : IsFutureCausal u) : + ‖u.spatialPart‖ ≤ u.timeComponent := by + obtain ⟨h1, h2⟩ := hu + rw [minkowskiProduct_self_eq_sq_sub] at h1 + nlinarith [norm_nonneg u.spatialPart] + +/-- The reverse Cauchy-Schwarz inequality: for future-directed causal `u`, `v`, + `√⟪u, u⟫ₘ √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ`. -/ +lemma sqrt_mul_sqrt_le_minkowskiProduct {d : ℕ} {u v : Vector d} (hu : IsFutureCausal u) + (hv : IsFutureCausal v) : √⟪u, u⟫ₘ * √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ := by + have hu' := norm_spatialPart_le_timeComponent hu + have hv' := norm_spatialPart_le_timeComponent hv + rw [minkowskiProduct_self_eq_sq_sub u, minkowskiProduct_self_eq_sq_sub v, + minkowskiProduct_eq_timeComponent_spatialPart u v] + have hcs := real_inner_le_norm u.spatialPart v.spatialPart + have := sqrt_mul_sqrt_le (norm_nonneg u.spatialPart) hu' (norm_nonneg v.spatialPart) hv' + linarith + +/-! + +## D. The reverse triangle inequality + +-/ + +/-- `⟪u + v, u + v⟫ₘ = ⟪u, u⟫ₘ + 2 ⟪u, v⟫ₘ + ⟪v, v⟫ₘ`. -/ +lemma minkowskiProduct_add_self {d : ℕ} (u v : Vector d) : + ⟪u + v, u + v⟫ₘ = ⟪u, u⟫ₘ + 2 * ⟪u, v⟫ₘ + ⟪v, v⟫ₘ := by + simp only [map_add, add_apply] + rw [minkowskiProduct_symm v u] + ring + +/-- The reverse triangle inequality: for future-directed causal `u`, `v`, + `√⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ`. -/ +lemma sqrt_add_sqrt_le_sqrt_add {d : ℕ} {u v : Vector d} (hu : IsFutureCausal u) + (hv : IsFutureCausal v) : √⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ := by + have hcs := sqrt_mul_sqrt_le_minkowskiProduct hu hv + have hsum : (√⟪u, u⟫ₘ + √⟪v, v⟫ₘ) ^ 2 ≤ ⟪u + v, u + v⟫ₘ := by + rw [minkowskiProduct_add_self, add_sq, Real.sq_sqrt hu.1, Real.sq_sqrt hv.1] + linarith + exact Real.le_sqrt_of_sq_le hsum + +/-- The sum of two future-directed causal vectors is future-directed causal. -/ +lemma isFutureCausal_add {d : ℕ} {u v : Vector d} (hu : IsFutureCausal u) (hv : IsFutureCausal v) : + IsFutureCausal (u + v) := by + refine ⟨?_, ?_⟩ + · have hcs := sqrt_mul_sqrt_le_minkowskiProduct hu hv + have hsq : 0 ≤ (√⟪u, u⟫ₘ + √⟪v, v⟫ₘ) ^ 2 := sq_nonneg _ + rw [add_sq, Real.sq_sqrt hu.1, Real.sq_sqrt hv.1] at hsq + rw [minkowskiProduct_add_self] + linarith + · show 0 ≤ (u + v) (Sum.inl 0) + rw [apply_add] + exact add_nonneg hu.2 hv.2 From af9c9ff3b2b3db7aaaf5b3a014cf73a42f2fe016 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 11:25:02 +0200 Subject: [PATCH 2/3] style(Relativity): use causallyFollows 0 u, file named after the structure, lemmas next to their definitions Applies the review remarks of #1642: the predicate IsFutureCausal is replaced by causallyFollows 0 u (equivalent), the file is renamed Causality/CausallyFollows.lean, the Minkowski product lemmas move to MinkowskiProduct.lean, the component lemmas to Vector/Basic.lean, and the elementary inequality is inlined in the proofs that use it. Co-authored-by: Claude Fable 5.1 --- Physlib.lean | 2 +- .../Relativity/Special/TwinParadox/Basic.lean | 6 +- .../Vector/Causality/CausallyFollows.lean | 160 ++++++++++++++++++ .../Vector/Causality/ReverseTriangle.lean | 150 ---------------- .../RealTensor/Vector/MinkowskiProduct.lean | 12 ++ 5 files changed, 176 insertions(+), 154 deletions(-) create mode 100644 Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean delete mode 100644 Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean diff --git a/Physlib.lean b/Physlib.lean index e5dd806bd8..623d49c086 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -468,8 +468,8 @@ public import Physlib.Relativity.Tensors.RealTensor.Units.Basic public import Physlib.Relativity.Tensors.RealTensor.Units.Pre public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.Basic +public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.CausallyFollows public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike -public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.ReverseTriangle public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Basic diff --git a/Physlib/Relativity/Special/TwinParadox/Basic.lean b/Physlib/Relativity/Special/TwinParadox/Basic.lean index b02f3ea903..c684ee020a 100644 --- a/Physlib/Relativity/Special/TwinParadox/Basic.lean +++ b/Physlib/Relativity/Special/TwinParadox/Basic.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.Special.ProperTime -public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.ReverseTriangle +public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.CausallyFollows /-! # Twin Paradox @@ -72,8 +72,8 @@ TODO "Find the conditions for which the age gap for the twin paradox is zero." Twin B: the age gap is nonnegative. This is the reverse triangle inequality of Minkowski space (`sqrt_add_sqrt_le_sqrt_add`) applied to the two legs of Twin B. -/ lemma ageGap_nonneg : 0 ≤ T.ageGap := by - have hu := isFutureCausal_of_causallyFollows T.twinBMid_causallyFollows_startPoint - have hv := isFutureCausal_of_causallyFollows T.endPoint_causallyFollows_twinBMid + have hu := causallyFollows_zero_sub T.twinBMid_causallyFollows_startPoint + have hv := causallyFollows_zero_sub T.endPoint_causallyFollows_twinBMid have h := sqrt_add_sqrt_le_sqrt_add hu hv have hsum : T.endPoint - T.startPoint = (T.twinBMid - T.startPoint) + (T.endPoint - T.twinBMid) := by abel diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean new file mode 100644 index 0000000000..f9e26a154a --- /dev/null +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean @@ -0,0 +1,160 @@ +/- +Copyright (c) 2026 Philippe Kevorkian. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Philippe Kevorkian +-/ +module + +public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike +public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike +/-! + +# Vectors in the causal future of the origin + +## i. Overview + +A vector `u` with `causallyFollows 0 u` is future-directed causal: time-like or light-like with a +nonnegative time component (`causallyFollows_zero_iff`). For two such vectors of Minkowski space +(signature `+---`), the Minkowski product dominates the product of the Minkowski norms, +`⟪u, v⟫ₘ ≥ √⟪u, u⟫ₘ √⟪v, v⟫ₘ` (reverse Cauchy-Schwarz inequality), and the Minkowski norm of the +sum dominates the sum of the norms, `√⟪u + v, u + v⟫ₘ ≥ √⟪u, u⟫ₘ + √⟪v, v⟫ₘ` (reverse triangle +inequality). The proofs reduce to the elementary inequality `√(a² - c²) √(b² - d²) ≤ a b - c d` for +`0 ≤ c ≤ a`, `0 ≤ d ≤ b`, applied to the time components and the Euclidean norms of the spatial +parts, together with the Euclidean Cauchy-Schwarz inequality. + +## ii. Key results + +- `causallyFollows_zero_iff`: `causallyFollows 0 u ↔ 0 ≤ ⟪u, u⟫ₘ ∧ 0 ≤ u⁰`; + `causallyFollows_zero_sub`: `q - p` is in the causal future of `0` when `q` causally follows `p`. +- `norm_spatialPart_le_timeComponent`: `‖u_spatial‖ ≤ u⁰`. +- `sqrt_mul_sqrt_le_minkowskiProduct`: the reverse Cauchy-Schwarz inequality. +- `sqrt_add_sqrt_le_sqrt_add`: the reverse triangle inequality; `causallyFollows_zero_add`. + +## iii. Table of contents + +- A. The causal future of the origin +- B. The reverse Cauchy-Schwarz inequality +- C. The reverse triangle inequality + +-/ + +@[expose] public section + +namespace Lorentz + +namespace Vector + +open InnerProductSpace + +/-! + +## A. The causal future of the origin + +-/ + +/-- A vector is in the causal future of the origin if and only if it is time-like or light-like + (`0 ≤ ⟪u, u⟫ₘ`) with a nonnegative time component. -/ +lemma causallyFollows_zero_iff {d : ℕ} {u : Vector d} : + causallyFollows 0 u ↔ 0 ≤ ⟪u, u⟫ₘ ∧ 0 ≤ u.timeComponent := by + simp only [causallyFollows, interiorFutureLightCone, futureLightConeBoundary, Set.mem_ofPred_eq, + sub_zero, timeLike_iff_norm_sq_pos, lightLike_iff_norm_sq_zero] + constructor + · rintro (⟨h1, h2⟩ | ⟨h1, h2⟩) + · exact ⟨h1.le, h2.le⟩ + · exact ⟨h1.ge, h2⟩ + · rintro ⟨h1, h2⟩ + rcases h1.lt_or_eq with h1 | h1 + · left + refine ⟨h1, lt_of_le_of_ne h2 fun h0 => ?_⟩ + have h := minkowskiProduct_self_le_timeComponent_sq u + have h0' : u.timeComponent = 0 := h0.symm + rw [h0'] at h + norm_num at h + linarith + · right + exact ⟨h1.symm, h2⟩ + +/-- The vector from `p` to `q` is in the causal future of the origin when `q` causally + follows `p`. -/ +lemma causallyFollows_zero_sub {d : ℕ} {p q : Vector d} (h : causallyFollows p q) : + causallyFollows 0 (q - p) := by + simpa only [causallyFollows, interiorFutureLightCone, futureLightConeBoundary, Set.mem_ofPred_eq, + sub_zero] using h + +/-! + +## B. The reverse Cauchy-Schwarz inequality + +-/ + +/-- For a vector in the causal future of the origin, the Euclidean norm of the spatial part is at + most the time component. -/ +lemma norm_spatialPart_le_timeComponent {d : ℕ} {u : Vector d} (hu : causallyFollows 0 u) : + ‖u.spatialPart‖ ≤ u.timeComponent := by + obtain ⟨h1, _⟩ := causallyFollows_zero_iff.mp hu + rw [minkowskiProduct_self_eq_sq_sub] at h1 + nlinarith [norm_nonneg u.spatialPart] + +/-- The reverse Cauchy-Schwarz inequality: for `u`, `v` in the causal future of the origin, + `√⟪u, u⟫ₘ √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ`. -/ +lemma sqrt_mul_sqrt_le_minkowskiProduct {d : ℕ} {u v : Vector d} (hu : causallyFollows 0 u) + (hv : causallyFollows 0 v) : √⟪u, u⟫ₘ * √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ := by + have hu' := norm_spatialPart_le_timeComponent hu + have hv' := norm_spatialPart_le_timeComponent hv + rw [minkowskiProduct_self_eq_sq_sub u, minkowskiProduct_self_eq_sq_sub v, + minkowskiProduct_eq_timeComponent_spatialPart u v] + have hcs := real_inner_le_norm u.spatialPart v.spatialPart + set a := u.timeComponent + set c := ‖u.spatialPart‖ + set b := v.timeComponent + set e := ‖v.spatialPart‖ + have hc0 : 0 ≤ c := norm_nonneg _ + have he0 : 0 ≤ e := norm_nonneg _ + have helem : √(a ^ 2 - c ^ 2) * √(b ^ 2 - e ^ 2) ≤ a * b - c * e := by + -- the elementary inequality `√(a² - c²) √(b² - e²) ≤ a b - c e` for `0 ≤ c ≤ a`, `0 ≤ e ≤ b`: + -- indeed `(a b - c e)² - (a² - c²)(b² - e²) = (a e - b c)²` + have h1 : 0 ≤ a ^ 2 - c ^ 2 := by nlinarith + have h2 : 0 ≤ a * b - c * e := by nlinarith + calc √(a ^ 2 - c ^ 2) * √(b ^ 2 - e ^ 2) = √((a ^ 2 - c ^ 2) * (b ^ 2 - e ^ 2)) := + (Real.sqrt_mul h1 _).symm + _ ≤ √((a * b - c * e) ^ 2) := Real.sqrt_le_sqrt (by nlinarith [sq_nonneg (a * e - b * c)]) + _ = a * b - c * e := Real.sqrt_sq h2 + linarith + +/-! + +## C. The reverse triangle inequality + +-/ + +/-- The reverse triangle inequality: for `u`, `v` in the causal future of the origin, + `√⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ`. -/ +lemma sqrt_add_sqrt_le_sqrt_add {d : ℕ} {u v : Vector d} (hu : causallyFollows 0 u) + (hv : causallyFollows 0 v) : √⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ := by + have hcs := sqrt_mul_sqrt_le_minkowskiProduct hu hv + have hu1 := (causallyFollows_zero_iff.mp hu).1 + have hv1 := (causallyFollows_zero_iff.mp hv).1 + have hsum : (√⟪u, u⟫ₘ + √⟪v, v⟫ₘ) ^ 2 ≤ ⟪u + v, u + v⟫ₘ := by + rw [minkowskiProduct_add_self, add_sq, Real.sq_sqrt hu1, Real.sq_sqrt hv1] + linarith + exact Real.le_sqrt_of_sq_le hsum + +/-- The sum of two vectors in the causal future of the origin is in the causal future of the + origin. -/ +lemma causallyFollows_zero_add {d : ℕ} {u v : Vector d} (hu : causallyFollows 0 u) + (hv : causallyFollows 0 v) : causallyFollows 0 (u + v) := by + obtain ⟨hu1, hu2⟩ := causallyFollows_zero_iff.mp hu + obtain ⟨hv1, hv2⟩ := causallyFollows_zero_iff.mp hv + refine causallyFollows_zero_iff.mpr ⟨?_, ?_⟩ + · have hcs := sqrt_mul_sqrt_le_minkowskiProduct hu hv + have hsq : 0 ≤ (√⟪u, u⟫ₘ + √⟪v, v⟫ₘ) ^ 2 := sq_nonneg _ + rw [add_sq, Real.sq_sqrt hu1, Real.sq_sqrt hv1] at hsq + rw [minkowskiProduct_add_self] + linarith + · show 0 ≤ (u + v) (Sum.inl 0) + rw [apply_add] + exact add_nonneg hu2 hv2 + +end Vector + +end Lorentz diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean deleted file mode 100644 index 3a0b8ec405..0000000000 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/ReverseTriangle.lean +++ /dev/null @@ -1,150 +0,0 @@ -/- -Copyright (c) 2026 Philippe Kevorkian. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Philippe Kevorkian --/ -module - -public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.TimeLike -public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike -/-! - -# The reverse Cauchy-Schwarz and reverse triangle inequalities - -## i. Overview - -For two future-directed causal vectors `u`, `v` of Minkowski space (signature `+---`), the -Minkowski product dominates the product of the Minkowski norms, `⟪u, v⟫ₘ ≥ √⟪u, u⟫ₘ √⟪v, v⟫ₘ` -(reverse Cauchy-Schwarz inequality), and the Minkowski norm of the sum dominates the sum of the -norms, `√⟪u + v, u + v⟫ₘ ≥ √⟪u, u⟫ₘ + √⟪v, v⟫ₘ` (reverse triangle inequality). The proof reduces to -the elementary inequality `√(a² - c²) √(b² - d²) ≤ a b - c d` for `0 ≤ c ≤ a`, `0 ≤ d ≤ b`, applied -to the time components and the Euclidean norms of the spatial parts, together with the Euclidean -Cauchy-Schwarz inequality. - -## ii. Key results - -- `IsFutureCausal`: `0 ≤ ⟪u, u⟫ₘ` and `0 ≤ u⁰`; `isFutureCausal_of_causallyFollows`. -- `sqrt_mul_sqrt_le`: the elementary inequality. -- `norm_spatialPart_le_timeComponent`: `‖u_spatial‖ ≤ u⁰` for `u` future causal. -- `sqrt_mul_sqrt_le_minkowskiProduct`: the reverse Cauchy-Schwarz inequality. -- `sqrt_add_sqrt_le_sqrt_add`: the reverse triangle inequality; `isFutureCausal_add`. - -## iii. Table of contents - -- A. Future-directed causal vectors -- B. The elementary inequality -- C. The reverse Cauchy-Schwarz inequality -- D. The reverse triangle inequality - --/ - -@[expose] public section - -namespace Lorentz - -namespace Vector - -open InnerProductSpace - -/-! - -## A. Future-directed causal vectors - --/ - -/-- A vector is future-directed causal if it is time-like or light-like (`0 ≤ ⟪u, u⟫ₘ`) with a - nonnegative time component. -/ -def IsFutureCausal {d : ℕ} (u : Vector d) : Prop := 0 ≤ ⟪u, u⟫ₘ ∧ 0 ≤ u.timeComponent - -/-- The vector from `p` to `q` is future-directed causal when `q` causally follows `p`. -/ -lemma isFutureCausal_of_causallyFollows {d : ℕ} {p q : Vector d} (h : causallyFollows p q) : - IsFutureCausal (q - p) := by - rcases h with h | h - · obtain ⟨h1, h2⟩ := h - exact ⟨((timeLike_iff_norm_sq_pos _).mp h1).le, h2.le⟩ - · obtain ⟨h1, h2⟩ := h - exact ⟨((lightLike_iff_norm_sq_zero _).mp h1).ge, h2⟩ - -/-! - -## B. The elementary inequality - --/ - -/-- For `0 ≤ c ≤ a` and `0 ≤ d ≤ b`, `√(a² - c²) √(b² - d²) ≤ a b - c d`: indeed - `(a b - c d)² - (a² - c²)(b² - d²) = (a d - b c)²`. -/ -lemma sqrt_mul_sqrt_le {a b c d : ℝ} (hc : 0 ≤ c) (hca : c ≤ a) (hd : 0 ≤ d) (hdb : d ≤ b) : - √(a ^ 2 - c ^ 2) * √(b ^ 2 - d ^ 2) ≤ a * b - c * d := by - have h1 : 0 ≤ a ^ 2 - c ^ 2 := by nlinarith - have h2 : 0 ≤ a * b - c * d := by nlinarith - calc √(a ^ 2 - c ^ 2) * √(b ^ 2 - d ^ 2) = √((a ^ 2 - c ^ 2) * (b ^ 2 - d ^ 2)) := - (Real.sqrt_mul h1 _).symm - _ ≤ √((a * b - c * d) ^ 2) := Real.sqrt_le_sqrt (by nlinarith [sq_nonneg (a * d - b * c)]) - _ = a * b - c * d := Real.sqrt_sq h2 - -/-! - -## C. The reverse Cauchy-Schwarz inequality - --/ - -/-- `⟪u, u⟫ₘ = (u⁰)² - ‖u_spatial‖²`. -/ -lemma minkowskiProduct_self_eq_sq_sub {d : ℕ} (u : Vector d) : - ⟪u, u⟫ₘ = u.timeComponent ^ 2 - ‖u.spatialPart‖ ^ 2 := by - rw [minkowskiProduct_self_eq_timeComponent_spatialPart, Real.norm_eq_abs, sq_abs] - -/-- For a future-directed causal vector, the Euclidean norm of the spatial part is at most the - time component. -/ -lemma norm_spatialPart_le_timeComponent {d : ℕ} {u : Vector d} (hu : IsFutureCausal u) : - ‖u.spatialPart‖ ≤ u.timeComponent := by - obtain ⟨h1, h2⟩ := hu - rw [minkowskiProduct_self_eq_sq_sub] at h1 - nlinarith [norm_nonneg u.spatialPart] - -/-- The reverse Cauchy-Schwarz inequality: for future-directed causal `u`, `v`, - `√⟪u, u⟫ₘ √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ`. -/ -lemma sqrt_mul_sqrt_le_minkowskiProduct {d : ℕ} {u v : Vector d} (hu : IsFutureCausal u) - (hv : IsFutureCausal v) : √⟪u, u⟫ₘ * √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ := by - have hu' := norm_spatialPart_le_timeComponent hu - have hv' := norm_spatialPart_le_timeComponent hv - rw [minkowskiProduct_self_eq_sq_sub u, minkowskiProduct_self_eq_sq_sub v, - minkowskiProduct_eq_timeComponent_spatialPart u v] - have hcs := real_inner_le_norm u.spatialPart v.spatialPart - have := sqrt_mul_sqrt_le (norm_nonneg u.spatialPart) hu' (norm_nonneg v.spatialPart) hv' - linarith - -/-! - -## D. The reverse triangle inequality - --/ - -/-- `⟪u + v, u + v⟫ₘ = ⟪u, u⟫ₘ + 2 ⟪u, v⟫ₘ + ⟪v, v⟫ₘ`. -/ -lemma minkowskiProduct_add_self {d : ℕ} (u v : Vector d) : - ⟪u + v, u + v⟫ₘ = ⟪u, u⟫ₘ + 2 * ⟪u, v⟫ₘ + ⟪v, v⟫ₘ := by - simp only [map_add, add_apply] - rw [minkowskiProduct_symm v u] - ring - -/-- The reverse triangle inequality: for future-directed causal `u`, `v`, - `√⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ`. -/ -lemma sqrt_add_sqrt_le_sqrt_add {d : ℕ} {u v : Vector d} (hu : IsFutureCausal u) - (hv : IsFutureCausal v) : √⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ := by - have hcs := sqrt_mul_sqrt_le_minkowskiProduct hu hv - have hsum : (√⟪u, u⟫ₘ + √⟪v, v⟫ₘ) ^ 2 ≤ ⟪u + v, u + v⟫ₘ := by - rw [minkowskiProduct_add_self, add_sq, Real.sq_sqrt hu.1, Real.sq_sqrt hv.1] - linarith - exact Real.le_sqrt_of_sq_le hsum - -/-- The sum of two future-directed causal vectors is future-directed causal. -/ -lemma isFutureCausal_add {d : ℕ} {u v : Vector d} (hu : IsFutureCausal u) (hv : IsFutureCausal v) : - IsFutureCausal (u + v) := by - refine ⟨?_, ?_⟩ - · have hcs := sqrt_mul_sqrt_le_minkowskiProduct hu hv - have hsq : 0 ≤ (√⟪u, u⟫ₘ + √⟪v, v⟫ₘ) ^ 2 := sq_nonneg _ - rw [add_sq, Real.sq_sqrt hu.1, Real.sq_sqrt hv.1] at hsq - rw [minkowskiProduct_add_self] - linarith - · show 0 ≤ (u + v) (Sum.inl 0) - rw [apply_add] - exact add_nonneg hu.2 hv.2 diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean index 6f75ee9259..07aa91fa50 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean @@ -172,6 +172,18 @@ lemma minkowskiProduct_self_le_timeComponent_sq {d : ℕ} (p : Vector d) : rw [minkowskiProduct_self_eq_timeComponent_spatialPart] simp +/-- `⟪u, u⟫ₘ = (u⁰)² - ‖u_spatial‖²`. -/ +lemma minkowskiProduct_self_eq_sq_sub {d : ℕ} (u : Vector d) : + ⟪u, u⟫ₘ = u.timeComponent ^ 2 - ‖u.spatialPart‖ ^ 2 := by + rw [minkowskiProduct_self_eq_timeComponent_spatialPart, Real.norm_eq_abs, sq_abs] + +/-- `⟪u + v, u + v⟫ₘ = ⟪u, u⟫ₘ + 2 ⟪u, v⟫ₘ + ⟪v, v⟫ₘ`. -/ +lemma minkowskiProduct_add_self {d : ℕ} (u v : Vector d) : + ⟪u + v, u + v⟫ₘ = ⟪u, u⟫ₘ + 2 * ⟪u, v⟫ₘ + ⟪v, v⟫ₘ := by + simp only [map_add, _root_.add_apply] + rw [minkowskiProduct_symm v u] + ring + @[simp] lemma minkowskiProduct_basis_left {d : ℕ} (μ : Fin 1 ⊕ Fin d) (p : Vector d) : ⟪basis μ, p⟫ₘ = minkowskiMatrix μ μ * p μ := by From 5d60cb3a86de17313303cad88a42e9e5d93c724a Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 12:16:30 +0200 Subject: [PATCH 3/3] style(Relativity): name the lemmas after their causallyFollows hypothesis As requested in the review of #1642: the lemmas of CausallyFollows.lean whose hypotheses are causallyFollows 0 u end with _of_causallyFollows. Co-authored-by: Claude Fable 5.1 --- .../Relativity/Special/TwinParadox/Basic.lean | 4 +-- .../Vector/Causality/CausallyFollows.lean | 32 ++++++++++--------- 2 files changed, 19 insertions(+), 17 deletions(-) diff --git a/Physlib/Relativity/Special/TwinParadox/Basic.lean b/Physlib/Relativity/Special/TwinParadox/Basic.lean index c684ee020a..c45202e136 100644 --- a/Physlib/Relativity/Special/TwinParadox/Basic.lean +++ b/Physlib/Relativity/Special/TwinParadox/Basic.lean @@ -70,11 +70,11 @@ TODO "Find the conditions for which the age gap for the twin paradox is zero." /-- In the twin paradox with instantaneous acceleration, Twin A is always at least as old as Twin B: the age gap is nonnegative. This is the reverse triangle inequality of Minkowski space - (`sqrt_add_sqrt_le_sqrt_add`) applied to the two legs of Twin B. -/ + (`sqrt_add_sqrt_le_sqrt_add_of_causallyFollows`) applied to the two legs of Twin B. -/ lemma ageGap_nonneg : 0 ≤ T.ageGap := by have hu := causallyFollows_zero_sub T.twinBMid_causallyFollows_startPoint have hv := causallyFollows_zero_sub T.endPoint_causallyFollows_twinBMid - have h := sqrt_add_sqrt_le_sqrt_add hu hv + have h := sqrt_add_sqrt_le_sqrt_add_of_causallyFollows hu hv have hsum : T.endPoint - T.startPoint = (T.twinBMid - T.startPoint) + (T.endPoint - T.twinBMid) := by abel unfold ageGap properTimeTwinA properTimeTwinB properTime diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean index f9e26a154a..8fabac1661 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Causality/CausallyFollows.lean @@ -26,9 +26,10 @@ parts, together with the Euclidean Cauchy-Schwarz inequality. - `causallyFollows_zero_iff`: `causallyFollows 0 u ↔ 0 ≤ ⟪u, u⟫ₘ ∧ 0 ≤ u⁰`; `causallyFollows_zero_sub`: `q - p` is in the causal future of `0` when `q` causally follows `p`. -- `norm_spatialPart_le_timeComponent`: `‖u_spatial‖ ≤ u⁰`. -- `sqrt_mul_sqrt_le_minkowskiProduct`: the reverse Cauchy-Schwarz inequality. -- `sqrt_add_sqrt_le_sqrt_add`: the reverse triangle inequality; `causallyFollows_zero_add`. +- `norm_spatialPart_le_timeComponent_of_causallyFollows`: `‖u_spatial‖ ≤ u⁰`. +- `sqrt_mul_sqrt_le_minkowskiProduct_of_causallyFollows`: the reverse Cauchy-Schwarz inequality. +- `sqrt_add_sqrt_le_sqrt_add_of_causallyFollows`: the reverse triangle inequality; + `causallyFollows_zero_add_of_causallyFollows`. ## iii. Table of contents @@ -89,18 +90,18 @@ lemma causallyFollows_zero_sub {d : ℕ} {p q : Vector d} (h : causallyFollows p /-- For a vector in the causal future of the origin, the Euclidean norm of the spatial part is at most the time component. -/ -lemma norm_spatialPart_le_timeComponent {d : ℕ} {u : Vector d} (hu : causallyFollows 0 u) : - ‖u.spatialPart‖ ≤ u.timeComponent := by +lemma norm_spatialPart_le_timeComponent_of_causallyFollows {d : ℕ} {u : Vector d} + (hu : causallyFollows 0 u) : ‖u.spatialPart‖ ≤ u.timeComponent := by obtain ⟨h1, _⟩ := causallyFollows_zero_iff.mp hu rw [minkowskiProduct_self_eq_sq_sub] at h1 nlinarith [norm_nonneg u.spatialPart] /-- The reverse Cauchy-Schwarz inequality: for `u`, `v` in the causal future of the origin, `√⟪u, u⟫ₘ √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ`. -/ -lemma sqrt_mul_sqrt_le_minkowskiProduct {d : ℕ} {u v : Vector d} (hu : causallyFollows 0 u) - (hv : causallyFollows 0 v) : √⟪u, u⟫ₘ * √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ := by - have hu' := norm_spatialPart_le_timeComponent hu - have hv' := norm_spatialPart_le_timeComponent hv +lemma sqrt_mul_sqrt_le_minkowskiProduct_of_causallyFollows {d : ℕ} {u v : Vector d} + (hu : causallyFollows 0 u) (hv : causallyFollows 0 v) : √⟪u, u⟫ₘ * √⟪v, v⟫ₘ ≤ ⟪u, v⟫ₘ := by + have hu' := norm_spatialPart_le_timeComponent_of_causallyFollows hu + have hv' := norm_spatialPart_le_timeComponent_of_causallyFollows hv rw [minkowskiProduct_self_eq_sq_sub u, minkowskiProduct_self_eq_sq_sub v, minkowskiProduct_eq_timeComponent_spatialPart u v] have hcs := real_inner_le_norm u.spatialPart v.spatialPart @@ -129,9 +130,10 @@ lemma sqrt_mul_sqrt_le_minkowskiProduct {d : ℕ} {u v : Vector d} (hu : causall /-- The reverse triangle inequality: for `u`, `v` in the causal future of the origin, `√⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ`. -/ -lemma sqrt_add_sqrt_le_sqrt_add {d : ℕ} {u v : Vector d} (hu : causallyFollows 0 u) - (hv : causallyFollows 0 v) : √⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ := by - have hcs := sqrt_mul_sqrt_le_minkowskiProduct hu hv +lemma sqrt_add_sqrt_le_sqrt_add_of_causallyFollows {d : ℕ} {u v : Vector d} + (hu : causallyFollows 0 u) (hv : causallyFollows 0 v) : + √⟪u, u⟫ₘ + √⟪v, v⟫ₘ ≤ √⟪u + v, u + v⟫ₘ := by + have hcs := sqrt_mul_sqrt_le_minkowskiProduct_of_causallyFollows hu hv have hu1 := (causallyFollows_zero_iff.mp hu).1 have hv1 := (causallyFollows_zero_iff.mp hv).1 have hsum : (√⟪u, u⟫ₘ + √⟪v, v⟫ₘ) ^ 2 ≤ ⟪u + v, u + v⟫ₘ := by @@ -141,12 +143,12 @@ lemma sqrt_add_sqrt_le_sqrt_add {d : ℕ} {u v : Vector d} (hu : causallyFollows /-- The sum of two vectors in the causal future of the origin is in the causal future of the origin. -/ -lemma causallyFollows_zero_add {d : ℕ} {u v : Vector d} (hu : causallyFollows 0 u) - (hv : causallyFollows 0 v) : causallyFollows 0 (u + v) := by +lemma causallyFollows_zero_add_of_causallyFollows {d : ℕ} {u v : Vector d} + (hu : causallyFollows 0 u) (hv : causallyFollows 0 v) : causallyFollows 0 (u + v) := by obtain ⟨hu1, hu2⟩ := causallyFollows_zero_iff.mp hu obtain ⟨hv1, hv2⟩ := causallyFollows_zero_iff.mp hv refine causallyFollows_zero_iff.mpr ⟨?_, ?_⟩ - · have hcs := sqrt_mul_sqrt_le_minkowskiProduct hu hv + · have hcs := sqrt_mul_sqrt_le_minkowskiProduct_of_causallyFollows hu hv have hsq : 0 ≤ (√⟪u, u⟫ₘ + √⟪v, v⟫ₘ) ^ 2 := sq_nonneg _ rw [add_sq, Real.sq_sqrt hu1, Real.sq_sqrt hv1] at hsq rw [minkowskiProduct_add_self]