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.

structure SpecialRelativity.InstantaneousTwinParadox : Type

The twin paradox assuming instantaneous acceleration.

• startPoint : SpaceTime

  The starting point of both twins.

• endPoint : SpaceTime

  The end point of both twins.

• twinBMid : SpaceTime

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

• endPoint_causallyFollows_startPoint : Lorentz.Vector.causallyFollows self.startPoint self.endPoint
• twinBMid_causallyFollows_startPoint : Lorentz.Vector.causallyFollows self.startPoint self.twinBMid
• endPoint_causallyFollows_twinBMid : Lorentz.Vector.causallyFollows self.twinBMid self.endPoint

def SpecialRelativity.InstantaneousTwinParadox.properTimeTwinA (T : InstantaneousTwinParadox) : ℝ

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

Equations

• T.properTimeTwinA = T.startPoint.properTime T.endPoint

def SpecialRelativity.InstantaneousTwinParadox.properTimeTwinB (T : InstantaneousTwinParadox) : ℝ

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.

Equations

• T.properTimeTwinB = T.startPoint.properTime T.twinBMid + T.twinBMid.properTime T.endPoint

def SpecialRelativity.InstantaneousTwinParadox.ageGap (T : InstantaneousTwinParadox) : ℝ

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

Equations

• T.ageGap = T.properTimeTwinA - T.properTimeTwinB

def SpecialRelativity.InstantaneousTwinParadox.ageGap_nonneg : InformalLemma

In the twin paradox with instantaneous acceleration, Twin A is always older then Twin B.

Equations

• SpecialRelativity.InstantaneousTwinParadox.ageGap_nonneg = { deps := [`SpecialRelativity.InstantaneousTwinParadox.ageGap], tag := "7ROVE" }

Example 1

def SpecialRelativity.InstantaneousTwinParadox.example1 : InstantaneousTwinParadox

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].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SpecialRelativity.InstantaneousTwinParadox.example1_properTimeTwinA : example1.properTimeTwinA = 15

@[simp]

theorem SpecialRelativity.InstantaneousTwinParadox.example1_properTimeTwinB : example1.properTimeTwinB = 9

theorem SpecialRelativity.InstantaneousTwinParadox.example1_ageGap : example1.ageGap = 6