Physlib.Relativity.Special.TwinParadox.Basic

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.Special.ProperTime

Twin Paradox

The twin paradox corresponds to the following scenario:

Two twins start at the same point startPoint in spacetime. Twin A travels at constant speed to the spacetime point endPoint, whilst twin B makes a detour through the spacetime twinBMid and then to endPoint.

In this file, we assume that both twins travel at constant speed, and that the acceleration of Twin B is instantaneous.

The conclusion of this scenario is that Twin A will be older than Twin B when they meet at endPoint. This is something we show here with an explicit example.

The origin of the twin paradox dates back to Paul Langevin in 1911.

@[expose] public section

The twin paradox assuming instantaneous acceleration.

The starting point of both twins.

The end point of both twins.

The point twin B travels to between the start point and the end point.

              structure InstantaneousTwinParadox where  startPoint : SpaceTime 3  endPoint : SpaceTime 3  twinBMid : SpaceTime 3
  endPoint_causallyFollows_startPoint : causallyFollows startPoint endPoint
  twinBMid_causallyFollows_startPoint : causallyFollows startPoint twinBMid
  endPoint_causallyFollows_twinBMid : causallyFollows twinBMid endPoint

The proper time experienced by twin A travelling at constant speed from T.startPoint to T.endPoint.

def properTimeTwinA : ℝ := SpaceTime.properTime T.startPoint T.endPoint

The proper time experienced by twin B travelling at constant speed from T.startPoint to T.twinBMid, and then from T.twinBMid to T.endPoint.

def properTimeTwinB : ℝ := SpaceTime.properTime T.startPoint T.twinBMid +
  SpaceTime.properTime T.twinBMid T.endPoint

The proper time of twin A minus the proper time of twin B.

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"

Example 1

The twin paradox in which:

Twin A starts at 0 and travels at constant speed to [15, 0, 0, 0].

Twin B starts at 0 and travels at constant speed to [7.5, 6, 0, 0] and then at (different) constant speed to [15, 0, 0, 0].


def example1 : InstantaneousTwinParadox where
  startPoint := 0
  endPoint := (fun
    | Sum.inl 0 => 15
    | Sum.inr i => 0)
  twinBMid := (fun
    | Sum.inl 0 => 7.5
    | Sum.inr 0 => 6
    | Sum.inr i => 0)
  endPoint_causallyFollows_startPoint := byT:InstantaneousTwinParadox⊢ causallyFollows 0 fun x =>
  match x with
  | Sum.inl 0 => 15
  | Sum.inr i => 0
    simp [causallyFollows]T:InstantaneousTwinParadox⊢ (fun x =>
      match x with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) ∈
    interiorFutureLightCone 0 ∨
  (fun x =>
      match x with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) ∈
    futureLightConeBoundary 0
    leftT:InstantaneousTwinParadox⊢ (fun x =>
    match x with
    | Sum.inl 0 => 15
    | Sum.inr i => 0) ∈
  interiorFutureLightCone 0
    simp only [interiorFutureLightCone, sub_zero, Fin.isValue, Set.mem_setOf_eq, Nat.ofNat_pos,
      and_true]T:InstantaneousTwinParadox⊢ (causalCharacter fun x =>
    match x with
    | Sum.inl 0 => 15
    | Sum.inr i => 0) =
  CausalCharacter.timeLike
    refine (timeLike_iff_norm_sq_pos _).mpr ?_T:InstantaneousTwinParadox⊢ 0 <
  (minkowskiProduct fun x =>
      match x with
      | Sum.inl 0 => 15
      | Sum.inr i => 0)
    fun x =>
    match x with
    | Sum.inl 0 => 15
    | Sum.inr i => 0
    rw [minkowskiProduct_toCoordT:InstantaneousTwinParadox⊢ 0 <
  ((match Sum.inl 0 with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) *
      match Sum.inl 0 with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) -
    ∑ i,
      (match Sum.inr i with
        | Sum.inl 0 => 15
        | Sum.inr i => 0) *
        match Sum.inr i with
        | Sum.inl 0 => 15
        | Sum.inr i => 0T:InstantaneousTwinParadox⊢ 0 <
  ((match Sum.inl 0 with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) *
      match Sum.inl 0 with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) -
    ∑ i,
      (match Sum.inr i with
        | Sum.inl 0 => 15
        | Sum.inr i => 0) *
        match Sum.inr i with
        | Sum.inl 0 => 15
        | Sum.inr i => 0]T:InstantaneousTwinParadox⊢ 0 <
  ((match Sum.inl 0 with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) *
      match Sum.inl 0 with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) -
    ∑ i,
      (match Sum.inr i with
        | Sum.inl 0 => 15
        | Sum.inr i => 0) *
        match Sum.inr i with
        | Sum.inl 0 => 15
        | Sum.inr i => 0
    simpAll goals completed! 🐙
  twinBMid_causallyFollows_startPoint := byT:InstantaneousTwinParadox⊢ causallyFollows 0 fun x =>
  match x with
  | Sum.inl 0 => 7.5
  | Sum.inr 0 => 6
  | Sum.inr i => 0
    simp only [causallyFollows]T:InstantaneousTwinParadox⊢ (fun x =>
      match x with
      | Sum.inl 0 => 7.5
      | Sum.inr 0 => 6
      | Sum.inr i => 0) ∈
    interiorFutureLightCone 0 ∨
  (fun x =>
      match x with
      | Sum.inl 0 => 7.5
      | Sum.inr 0 => 6
      | Sum.inr i => 0) ∈
    futureLightConeBoundary 0
    leftT:InstantaneousTwinParadox⊢ (fun x =>
    match x with
    | Sum.inl 0 => 7.5
    | Sum.inr 0 => 6
    | Sum.inr i => 0) ∈
  interiorFutureLightCone 0
    simp only [interiorFutureLightCone, sub_zero, Fin.isValue, Set.mem_setOf_eq]T:InstantaneousTwinParadox⊢ (causalCharacter fun x =>
      match x with
      | Sum.inl 0 => 7.5
      | Sum.inr 0 => 6
      | Sum.inr i => 0) =
    CausalCharacter.timeLike ∧
  0 < 7.5
    norm_numT:InstantaneousTwinParadox⊢ (causalCharacter fun x =>
    match x with
    | Sum.inl 0 => 15 / 2
    | Sum.inr 0 => 6
    | Sum.inr i => 0) =
  CausalCharacter.timeLike
    refine (timeLike_iff_norm_sq_pos _).mpr ?_T:InstantaneousTwinParadox⊢ 0 <
  (minkowskiProduct fun x =>
      match x with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0)
    fun x =>
    match x with
    | Sum.inl 0 => 15 / 2
    | Sum.inr 0 => 6
    | Sum.inr i => 0
    rw [minkowskiProduct_toCoordT:InstantaneousTwinParadox⊢ 0 <
  ((match Sum.inl 0 with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0) *
      match Sum.inl 0 with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0) -
    ∑ i,
      (match Sum.inr i with
        | Sum.inl 0 => 15 / 2
        | Sum.inr 0 => 6
        | Sum.inr i => 0) *
        match Sum.inr i with
        | Sum.inl 0 => 15 / 2
        | Sum.inr 0 => 6
        | Sum.inr i => 0T:InstantaneousTwinParadox⊢ 0 <
  ((match Sum.inl 0 with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0) *
      match Sum.inl 0 with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0) -
    ∑ i,
      (match Sum.inr i with
        | Sum.inl 0 => 15 / 2
        | Sum.inr 0 => 6
        | Sum.inr i => 0) *
        match Sum.inr i with
        | Sum.inl 0 => 15 / 2
        | Sum.inr 0 => 6
        | Sum.inr i => 0]T:InstantaneousTwinParadox⊢ 0 <
  ((match Sum.inl 0 with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0) *
      match Sum.inl 0 with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0) -
    ∑ i,
      (match Sum.inr i with
        | Sum.inl 0 => 15 / 2
        | Sum.inr 0 => 6
        | Sum.inr i => 0) *
        match Sum.inr i with
        | Sum.inl 0 => 15 / 2
        | Sum.inr 0 => 6
        | Sum.inr i => 0
    simp [Fin.sum_univ_three]T:InstantaneousTwinParadox⊢ 6 * 6 < 15 / 2 * (15 / 2)
    norm_numAll goals completed! 🐙
  endPoint_causallyFollows_twinBMid := byT:InstantaneousTwinParadox⊢ causallyFollows
  (fun x =>
    match x with
    | Sum.inl 0 => 7.5
    | Sum.inr 0 => 6
    | Sum.inr i => 0)
  fun x =>
  match x with
  | Sum.inl 0 => 15
  | Sum.inr i => 0
    simp [causallyFollows]T:InstantaneousTwinParadox⊢ ((fun x =>
      match x with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) ∈
    interiorFutureLightCone fun x =>
      match x with
      | Sum.inl 0 => 7.5
      | Sum.inr 0 => 6
      | Sum.inr i => 0) ∨
  (fun x =>
      match x with
      | Sum.inl 0 => 15
      | Sum.inr i => 0) ∈
    futureLightConeBoundary fun x =>
      match x with
      | Sum.inl 0 => 7.5
      | Sum.inr 0 => 6
      | Sum.inr i => 0
    leftT:InstantaneousTwinParadox⊢ (fun x =>
    match x with
    | Sum.inl 0 => 15
    | Sum.inr i => 0) ∈
  interiorFutureLightCone fun x =>
    match x with
    | Sum.inl 0 => 7.5
    | Sum.inr 0 => 6
    | Sum.inr i => 0
    simp [interiorFutureLightCone]T:InstantaneousTwinParadox⊢ ((fun x =>
          match x with
          | Sum.inl 0 => 15
          | Sum.inr i => 0) -
        fun x =>
        match x with
        | Sum.inl 0 => 7.5
        | Sum.inr 0 => 6
        | Sum.inr i => 0).causalCharacter =
    CausalCharacter.timeLike ∧
  7.5 < 15
    norm_numT:InstantaneousTwinParadox⊢ ((fun x =>
        match x with
        | Sum.inl 0 => 15
        | Sum.inr i => 0) -
      fun x =>
      match x with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0).causalCharacter =
  CausalCharacter.timeLike
    refine (timeLike_iff_norm_sq_pos _).mpr ?_T:InstantaneousTwinParadox⊢ 0 <
  (minkowskiProduct
      ((fun x =>
          match x with
          | Sum.inl 0 => 15
          | Sum.inr i => 0) -
        fun x =>
        match x with
        | Sum.inl 0 => 15 / 2
        | Sum.inr 0 => 6
        | Sum.inr i => 0))
    ((fun x =>
        match x with
        | Sum.inl 0 => 15
        | Sum.inr i => 0) -
      fun x =>
      match x with
      | Sum.inl 0 => 15 / 2
      | Sum.inr 0 => 6
      | Sum.inr i => 0)
    rw [minkowskiProduct_toCoordT:InstantaneousTwinParadox⊢ 0 <
  ((fun x =>
            match x with
            | Sum.inl 0 => 15
            | Sum.inr i => 0) -
          fun x =>
          match x with
          | Sum.inl 0 => 15 / 2
          | Sum.inr 0 => 6
          | Sum.inr i => 0)
        (Sum.inl 0) *
      ((fun x =>
            match x with
            | Sum.inl 0 => 15
            | Sum.inr i => 0) -
          fun x =>
          match x with
          | Sum.inl 0 => 15 / 2
          | Sum.inr 0 => 6
          | Sum.inr i => 0)
        (Sum.inl 0) -
    ∑ i,
      ((fun x =>
              match x with
              | Sum.inl 0 => 15
              | Sum.inr i => 0) -
            fun x =>
            match x with
            | Sum.inl 0 => 15 / 2
            | Sum.inr 0 => 6
            | Sum.inr i => 0)
          (Sum.inr i) *
        ((fun x =>
              match x with
              | Sum.inl 0 => 15
              | Sum.inr i => 0) -
            fun x =>
            match x with
            | Sum.inl 0 => 15 / 2
            | Sum.inr 0 => 6
            | Sum.inr i => 0)
          (Sum.inr i)T:InstantaneousTwinParadox⊢ 0 <
  ((fun x =>
            match x with
            | Sum.inl 0 => 15
            | Sum.inr i => 0) -
          fun x =>
          match x with
          | Sum.inl 0 => 15 / 2
          | Sum.inr 0 => 6
          | Sum.inr i => 0)
        (Sum.inl 0) *
      ((fun x =>
            match x with
            | Sum.inl 0 => 15
            | Sum.inr i => 0) -
          fun x =>
          match x with
          | Sum.inl 0 => 15 / 2
          | Sum.inr 0 => 6
          | Sum.inr i => 0)
        (Sum.inl 0) -
    ∑ i,
      ((fun x =>
              match x with
              | Sum.inl 0 => 15
              | Sum.inr i => 0) -
            fun x =>
            match x with
            | Sum.inl 0 => 15 / 2
            | Sum.inr 0 => 6
            | Sum.inr i => 0)
          (Sum.inr i) *
        ((fun x =>
              match x with
              | Sum.inl 0 => 15
              | Sum.inr i => 0) -
            fun x =>
            match x with
            | Sum.inl 0 => 15 / 2
            | Sum.inr 0 => 6
            | Sum.inr i => 0)
          (Sum.inr i)]T:InstantaneousTwinParadox⊢ 0 <
  ((fun x =>
            match x with
            | Sum.inl 0 => 15
            | Sum.inr i => 0) -
          fun x =>
          match x with
          | Sum.inl 0 => 15 / 2
          | Sum.inr 0 => 6
          | Sum.inr i => 0)
        (Sum.inl 0) *
      ((fun x =>
            match x with
            | Sum.inl 0 => 15
            | Sum.inr i => 0) -
          fun x =>
          match x with
          | Sum.inl 0 => 15 / 2
          | Sum.inr 0 => 6
          | Sum.inr i => 0)
        (Sum.inl 0) -
    ∑ i,
      ((fun x =>
              match x with
              | Sum.inl 0 => 15
              | Sum.inr i => 0) -
            fun x =>
            match x with
            | Sum.inl 0 => 15 / 2
            | Sum.inr 0 => 6
            | Sum.inr i => 0)
          (Sum.inr i) *
        ((fun x =>
              match x with
              | Sum.inl 0 => 15
              | Sum.inr i => 0) -
            fun x =>
            match x with
            | Sum.inl 0 => 15 / 2
            | Sum.inr 0 => 6
            | Sum.inr i => 0)
          (Sum.inr i)
    simp [Fin.sum_univ_three]T:InstantaneousTwinParadox⊢ 6 * 6 < (15 - 15 / 2) * (15 - 15 / 2)
    norm_numAll goals completed! 🐙

              @[simp]
lemma example1_properTimeTwinA : example1.properTimeTwinA = 15 := by⊢ example1.properTimeTwinA = 15
  simp [properTimeTwinA, example1, properTime, minkowskiProduct_toCoord]All goals completed! 🐙@[simp]
lemma example1_properTimeTwinB : example1.properTimeTwinB = 9 := by⊢ example1.properTimeTwinB = 9
  simp [properTimeTwinB, properTime, example1, minkowskiProduct_toCoord, Fin.sum_univ_three]⊢ √(7.5 * 7.5 - 6 * 6) + √(15 * (15 - 7.5) - (7.5 * (15 - 7.5) + 6 * 6)) = 9
  norm_num [show √81 = 9 from sqrt_eq_cases.mpr (by⊢ 9 * 9 = 81 ∧ 0 ≤ 9 ∨ 81 < 0 ∧ 9 = 0 norm_numAll goals completed! 🐙),
    show √4 = 2 from sqrt_eq_cases.mpr (by⊢ 2 * 2 = 4 ∧ 0 ≤ 2 ∨ 4 < 0 ∧ 2 = 0 norm_numAll goals completed! 🐙)]lemma example1_ageGap : example1.ageGap = 6 := by⊢ example1.ageGap = 6
  norm_num [ageGap]All goals completed! 🐙TODO "Do the twin paradox with a non-instantaneous acceleration. This should be done
  in a different module."