Physlib.SpaceAndTime.Time.TimeTransMan

Physlib
SpaceAndTime
Time
TimeTransMan

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 Mathlib.Geometry.Manifold.Diffeomorph
public import Physlib.SpaceAndTime.Time.Basic
public import Physlib.SpaceAndTime.Time.TimeUnit

The time manifold with a transitive action of `ℝ`

In this module we define the type TimeTransMan. This type physically corresponds to the manifold of time (diffeomorphic to ℝ) with the following additional structure:

a transitive action of ℝ,

a choice of orientation.

The manifold TimeTransMan is not equipped with a translationally-invariant metric. Such metrics are in one-to-one correspondence (to be shown) with positive reals, and as such we define the type TimeUnit (equivalent to the positive reals) to represent the choice of metric on TimeTransMan. This is defined in a different module.

From the point of view of physics, this choice of metric corresponds to a choice of units, hence the name, and we will use the phrase 'units of time' interchangeably 'choice of metric'.

Given a x : TimeUnit, and the structure above, we can define the following operations on TimeTransMan:

diff x t1 t2, for t1 t2 : TimeTransMan gives the signed difference between two points in time in the units x.

addTime x r t, for r : ℝ and t : TimeTransMan, gives the point in TimeTransMan that separated from t, by r in the unit x. For example, if x is the unit of seconds, then addTime x 1 t gives the point in TimeTransMan that is one second after t.

neg zero t, for a given zero : TimeTransMan, gives the point in TimeTransMan that is the same distance away from zero as t but in the opposite direction. This is defined using a choice of units, but is independent of the choice.

Recall that the type Time corresponds to the manifold of time with a given (but arbitrary) choice of units and origin (and therefore has a structure of a module over ℝ). Here we define the homeomorphism:

toTime zero x from TimeTransMan to Time where zero : TimeTransMan is the choice of origin and x : TimeUnit is the choice of units. This map is a diffeomorphism (to be shown).

@[expose] public section

The type TimeTransMan represents the time manifold with an orientation and a transitive action of the reals.

The choice of a map from TimeTransMan to ℝ.

structure TimeTransMan where val : ℝ

@[ext]
lemma ext_of {t1 t2 : TimeTransMan} (h : t1.val = t2.val) :
    t1 = t2 := byt1:TimeTransMant2:TimeTransManh:t1.val = t2.val⊢ t1 = t2
  cases t1mkt2:TimeTransManval✝:ℝh:{ val := val✝ }.val = t2.val⊢ { val := val✝ } = t2; cases t2mk.mkval✝¹:ℝval✝:ℝh:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ }; simp_allAll goals completed! 🐙

The topology on TimeTransMan.

The topology on TimeTransMan is induced from the topology on ℝ, via the choice of map TimeTransMan.val.

The instance of a topological space on TimeTransMan induced by the map TimeTransMan.val.

instance : TopologicalSpace TimeTransMan := TopologicalSpace.induced TimeTransMan.val
  PseudoMetricSpace.toUniformSpace.toTopologicalSpace

              lemma val_surjective : Function.Surjective TimeTransMan.val := by⊢ Function.Surjective val
  intro tt:ℝ⊢ ∃ a, a.val = t
  use { val := t }All goals completed! 🐙@[simp]
lemma val_range : Set.range val = Set.univ := by⊢ Set.range val = Set.univ
  refine Set.range_eq_univ.mpr val_surjectiveAll goals completed! 🐙lemma val_inducing : Topology.IsInducing TimeTransMan.val where
  eq_induced := rfllemma val_injective : Function.Injective TimeTransMan.val := by⊢ Function.Injective val
  intro t1 t2 ht1:TimeTransMant2:TimeTransManh:t1.val = t2.val⊢ t1 = t2
  cases t1mkt2:TimeTransManval✝:ℝh:{ val := val✝ }.val = t2.val⊢ { val := val✝ } = t2
  cases t2mk.mkval✝¹:ℝval✝:ℝh:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ }
  simp_allAll goals completed! 🐙lemma val_isOpenEmbedding : Topology.IsOpenEmbedding TimeTransMan.val where
  eq_induced := rfl
  isOpen_range := by⊢ IsOpen (Set.range val)
    simpAll goals completed! 🐙
  injective := val_injectivelemma isOpen_iff {s : Set TimeTransMan} :
    IsOpen s ↔ IsOpen (TimeTransMan.val '' s) :=
  Topology.IsOpenEmbedding.isOpen_iff_image_isOpen val_isOpenEmbedding

The choice of map Time.val from TimeTransMan to ℝ as a homeomorphism.


def valHomeomorphism : TimeTransMan ≃ₜ ℝ where
  toFun := TimeTransMan.val
  invFun := fun t => { val := t }
  left_inv := by⊢ Function.LeftInverse (fun t => { val := t }) val
    intro tt:TimeTransMan⊢ (fun t => { val := t }) t.val = t
    cases tmkval✝:ℝ⊢ (fun t => { val := t }) { val := val✝ }.val = { val := val✝ }
    rflAll goals completed! 🐙
  right_inv := by⊢ Function.RightInverse (fun t => { val := t }) val
    intro tt:ℝ⊢ ((fun t => { val := t }) t).val = t
    rflAll goals completed! 🐙
  continuous_toFun := by⊢ Continuous val fun_propAll goals completed! 🐙
  continuous_invFun := by⊢ Continuous fun t => { val := t }
    refine { isOpen_preimage := ?_ }⊢ ∀ (s : Set TimeTransMan), IsOpen s → IsOpen ((fun t => { val := t }) ⁻¹' s)
    intro s hss:Set TimeTransManhs:IsOpen s⊢ IsOpen ((fun t => { val := t }) ⁻¹' s)
    rw [isOpen_iffs:Set TimeTransManhs:IsOpen (val '' s)⊢ IsOpen ((fun t => { val := t }) ⁻¹' s)s:Set TimeTransManhs:IsOpen (val '' s)⊢ IsOpen ((fun t => { val := t }) ⁻¹' s)] at hss:Set TimeTransManhs:IsOpen (val '' s)⊢ IsOpen ((fun t => { val := t }) ⁻¹' s)
    rw [← Set.image_eq_preimage_of_inverses:Set TimeTransManhs:IsOpen (val '' s)⊢ IsOpen (?m.66 '' s)h₁s:Set TimeTransManhs:IsOpen (val '' s)⊢ Function.LeftInverse (fun t => { val := t }) ?m.66h₂s:Set TimeTransManhs:IsOpen (val '' s)⊢ Function.RightInverse (fun t => { val := t }) ?m.66s:Set TimeTransManhs:IsOpen (val '' s)⊢ TimeTransMan → ℝs:Set TimeTransManhs:IsOpen (val '' s)⊢ IsOpen (?m.66 '' s)h₁s:Set TimeTransManhs:IsOpen (val '' s)⊢ Function.LeftInverse (fun t => { val := t }) ?m.66h₂s:Set TimeTransManhs:IsOpen (val '' s)⊢ Function.RightInverse (fun t => { val := t }) ?m.66s:Set TimeTransManhs:IsOpen (val '' s)⊢ TimeTransMan → ℝ]s:Set TimeTransManhs:IsOpen (val '' s)⊢ IsOpen (?m.66 '' s)h₁s:Set TimeTransManhs:IsOpen (val '' s)⊢ Function.LeftInverse (fun t => { val := t }) ?m.66h₂s:Set TimeTransManhs:IsOpen (val '' s)⊢ Function.RightInverse (fun t => { val := t }) ?m.66s:Set TimeTransManhs:IsOpen (val '' s)⊢ TimeTransMan → ℝ
    ·s:Set TimeTransManhs:IsOpen (val '' s)⊢ IsOpen (?m.66 '' s) exact hsAll goals completed! 🐙
    ·h₁s:Set TimeTransManhs:IsOpen (val '' s)⊢ Function.LeftInverse (fun t => { val := t }) val intro th₁s:Set TimeTransManhs:IsOpen (val '' s)t:TimeTransMan⊢ (fun t => { val := t }) t.val = t
      rflAll goals completed! 🐙
    ·h₂s:Set TimeTransManhs:IsOpen (val '' s)⊢ Function.RightInverse (fun t => { val := t }) val intro xh₂s:Set TimeTransManhs:IsOpen (val '' s)x:ℝ⊢ ((fun t => { val := t }) x).val = x
      simpAll goals completed! 🐙

The manifold structure on TimeTransMan

The structure of a charted space on TimeTransMan

instance : ChartedSpace ℝ TimeTransMan where
  atlas := { valHomeomorphism.toOpenPartialHomeomorph }
  chartAt _ := valHomeomorphism.toOpenPartialHomeomorph
  mem_chart_source := by⊢ ∀ (x : TimeTransMan), x ∈ valHomeomorphism.toOpenPartialHomeomorph.source
    simpAll goals completed! 🐙
  chart_mem_atlas := by⊢ ∀ (x : TimeTransMan), valHomeomorphism.toOpenPartialHomeomorph ∈ {valHomeomorphism.toOpenPartialHomeomorph}
    intro xx:TimeTransMan⊢ valHomeomorphism.toOpenPartialHomeomorph ∈ {valHomeomorphism.toOpenPartialHomeomorph}
    simpAll goals completed! 🐙

The structure of a manifold on TimeTransMan induced by the choice of map Time.val.

instance : IsManifold 𝓘(ℝ, ℝ) ω TimeTransMan where
  compatible := by⊢ ∀ {e e' : OpenPartialHomeomorph TimeTransMan ℝ},
  e ∈ atlas ℝ TimeTransMan → e' ∈ atlas ℝ TimeTransMan → e.symm ≫ₕ e' ∈ contDiffGroupoid ω 𝓘(ℝ, ℝ)
    intro e1 e2 h1 h2e1:OpenPartialHomeomorph TimeTransMan ℝe2:OpenPartialHomeomorph TimeTransMan ℝh1:e1 ∈ atlas ℝ TimeTransManh2:e2 ∈ atlas ℝ TimeTransMan⊢ e1.symm ≫ₕ e2 ∈ contDiffGroupoid ω 𝓘(ℝ, ℝ)
    simp [atlas, ChartedSpace.atlas] at h1 h2e1:OpenPartialHomeomorph TimeTransMan ℝe2:OpenPartialHomeomorph TimeTransMan ℝh1:e1 = valHomeomorphism.toOpenPartialHomeomorphh2:e2 = valHomeomorphism.toOpenPartialHomeomorph⊢ e1.symm ≫ₕ e2 ∈ contDiffGroupoid ω 𝓘(ℝ, ℝ)
    subst h1 h2⊢ valHomeomorphism.toOpenPartialHomeomorph.symm ≫ₕ valHomeomorphism.toOpenPartialHomeomorph ∈ contDiffGroupoid ω 𝓘(ℝ, ℝ)
    exact symm_trans_mem_contDiffGroupoid valHomeomorphism.toOpenPartialHomeomorphAll goals completed! 🐙

lemma val_contDiff : ContMDiff 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ω TimeTransMan.val := by⊢ ContMDiff 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ω val
  refine contMDiffOn_univ.mp ?_⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ω val Set.univ
  exact contMDiffOn_chart (x := (⟨0⟩ : TimeTransMan))All goals completed! 🐙

The transitive group action on TimeTransMan

              instance : VAdd ℝ TimeTransMan where
  vadd p t := { val := p + t.val }@[simp]
lemma vadd_val (p : ℝ) (t : TimeTransMan) :
    (p +ᵥ t).val = p + t.val := rflinstance : AddAction ℝ TimeTransMan where
  zero_vadd t := byt:TimeTransMan⊢ 0 +ᵥ t = t
    cases tmkval✝:ℝ⊢ 0 +ᵥ { val := val✝ } = { val := val✝ }
    extmkval✝:ℝ⊢ (0 +ᵥ { val := val✝ }).val = { val := val✝ }.val
    simpAll goals completed! 🐙
  add_vadd p1 p2 t := byp1:ℝp2:ℝt:TimeTransMan⊢ (p1 + p2) +ᵥ t = p1 +ᵥ p2 +ᵥ t
    extp1:ℝp2:ℝt:TimeTransMan⊢ ((p1 + p2) +ᵥ t).val = (p1 +ᵥ p2 +ᵥ t).val
    simp only [vadd_val]p1:ℝp2:ℝt:TimeTransMan⊢ p1 + p2 + t.val = p1 + (p2 + t.val)
    ringAll goals completed! 🐙

A choice of orientation on TimeTransMan

              instance : LE TimeTransMan where
  le x y := x.val ≤ y.vallemma le_def (t1 t2 : TimeTransMan) :
    t1 ≤ t2 ↔ t1.val ≤ t2.val := Iff.rflinstance : Nonempty TimeTransMan := Nonempty.intro ⟨0⟩

Functions based on a choice of unit

Signed difference

              

lemma diff_eq_val (x : TimeUnit) (t1 t2 : TimeTransMan) :
    diff x t1 t2 = 1/x.val * (t1.val - t2.val) := byx:TimeUnitt1:TimeTransMant2:TimeTransMan⊢ diff x t1 t2 = 1 / x.val * (t1.val - t2.val)
  by_cases h : t2 ≤ t1posx:TimeUnitt1:TimeTransMant2:TimeTransManh:t2 ≤ t1⊢ diff x t1 t2 = 1 / x.val * (t1.val - t2.val)negx:TimeUnitt1:TimeTransMant2:TimeTransManh:¬t2 ≤ t1⊢ diff x t1 t2 = 1 / x.val * (t1.val - t2.val)
  ·posx:TimeUnitt1:TimeTransMant2:TimeTransManh:t2 ≤ t1⊢ diff x t1 t2 = 1 / x.val * (t1.val - t2.val) simp [diff, dist, h]posx:TimeUnitt1:TimeTransMant2:TimeTransManh:t2 ≤ t1⊢ t2.val ≤ t1.val
    simpa [le_def] using hAll goals completed! 🐙
  ·negx:TimeUnitt1:TimeTransMant2:TimeTransManh:¬t2 ≤ t1⊢ diff x t1 t2 = 1 / x.val * (t1.val - t2.val) simp [diff, dist, h]negx:TimeUnitt1:TimeTransMant2:TimeTransManh:¬t2 ≤ t1⊢ -(x.val⁻¹ * |t1.val - t2.val|) = x.val⁻¹ * (t1.val - t2.val)
    simp [le_def] at hnegx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ -(x.val⁻¹ * |t1.val - t2.val|) = x.val⁻¹ * (t1.val - t2.val)
    rw [abs_of_negnegx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ -(x.val⁻¹ * -(t1.val - t2.val)) = x.val⁻¹ * (t1.val - t2.val)negx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ t1.val - t2.val < 0negx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ -(x.val⁻¹ * -(t1.val - t2.val)) = x.val⁻¹ * (t1.val - t2.val)negx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ t1.val - t2.val < 0]negx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ -(x.val⁻¹ * -(t1.val - t2.val)) = x.val⁻¹ * (t1.val - t2.val)negx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ t1.val - t2.val < 0
    have hx : x.val ≠ 0 := x.val_ne_zeronegx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.valhx:x.val ≠ 0⊢ -(x.val⁻¹ * -(t1.val - t2.val)) = x.val⁻¹ * (t1.val - t2.val)negx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ t1.val - t2.val < 0
    field_simpnegx:TimeUnitt1:TimeTransMant2:TimeTransManh:t1.val < t2.val⊢ t1.val - t2.val < 0
    linarithAll goals completed! 🐙@[simp]
lemma diff_self (x : TimeUnit) (t : TimeTransMan) :
    diff x t t = 0 := byx:TimeUnitt:TimeTransMan⊢ diff x t t = 0
  simp [diff_eq_val]All goals completed! 🐙

lemma diff_fst_injective (x : TimeUnit) (t : TimeTransMan) : Function.Injective (diff x · t) := byx:TimeUnitt:TimeTransMan⊢ Function.Injective fun x_1 => diff x x_1 t
  intro t1 t2 hx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(fun x_1 => diff x x_1 t) t1 = (fun x_1 => diff x x_1 t) t2⊢ t1 = t2
  simp [diff] at hx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2⊢ t1 = t2
  by_cases h1 : t ≤ t1posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:t ≤ t1⊢ t1 = t2negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:¬t ≤ t1⊢ t1 = t2
    <;>posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:t ≤ t1⊢ t1 = t2negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:¬t ≤ t1⊢ t1 = t2 by_cases h2 : t ≤ t2posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:¬t ≤ t1h2:t ≤ t2⊢ t1 = t2negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:¬t ≤ t1h2:¬t ≤ t2⊢ t1 = t2
  ·posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:t ≤ t1h2:t ≤ t2⊢ t1 = t2 simp_all [dist, le_def]posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:|t1.val - t.val| = |t2.val - t.val|h1:t.val ≤ t1.valh2:t.val ≤ t2.val⊢ t1 = t2
    rw [abs_of_nonneg (byx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:|t1.val - t.val| = |t2.val - t.val|h1:t.val ≤ t1.valh2:t.val ≤ t2.val⊢ 0 ≤ t1.val - t.valposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:t1.val - t.val = t2.val - t.valh1:t.val ≤ t1.valh2:t.val ≤ t2.val⊢ t1 = t2 linarithAll goals completed! 🐙posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:t1.val - t.val = t2.val - t.valh1:t.val ≤ t1.valh2:t.val ≤ t2.val⊢ t1 = t2), abs_of_nonneg (byx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:t1.val - t.val = |t2.val - t.val|h1:t.val ≤ t1.valh2:t.val ≤ t2.val⊢ 0 ≤ t2.val - t.valposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:t1.val - t.val = t2.val - t.valh1:t.val ≤ t1.valh2:t.val ≤ t2.val⊢ t1 = t2 linarithAll goals completed! 🐙posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:t1.val - t.val = t2.val - t.valh1:t.val ≤ t1.valh2:t.val ≤ t2.val⊢ t1 = t2)] at hposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:t1.val - t.val = t2.val - t.valh1:t.val ≤ t1.valh2:t.val ≤ t2.val⊢ t1 = t2
    simp at hposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh1:t.val ≤ t1.valh2:t.val ≤ t2.valh:t1.val = t2.val⊢ t1 = t2
    extposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh1:t.val ≤ t1.valh2:t.val ≤ t2.valh:t1.val = t2.val⊢ t1.val = t2.val
    exact hAll goals completed! 🐙
  ·negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:t ≤ t1h2:¬t ≤ t2⊢ t1 = t2 simp_all [dist, le_def]negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:x.val⁻¹ * |t1.val - t.val| = -(x.val⁻¹ * |t2.val - t.val|)h1:t.val ≤ t1.valh2:t2.val < t.val⊢ t1 = t2
    rw [abs_of_nonneg (byx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:x.val⁻¹ * |t1.val - t.val| = -(x.val⁻¹ * |t2.val - t.val|)h1:t.val ≤ t1.valh2:t2.val < t.val⊢ 0 ≤ t1.val - t.valnegx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:x.val⁻¹ * (t1.val - t.val) = -(x.val⁻¹ * -(t2.val - t.val))h1:t.val ≤ t1.valh2:t2.val < t.val⊢ t1 = t2 linarithAll goals completed! 🐙negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:x.val⁻¹ * (t1.val - t.val) = -(x.val⁻¹ * -(t2.val - t.val))h1:t.val ≤ t1.valh2:t2.val < t.val⊢ t1 = t2), abs_of_neg (byx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:x.val⁻¹ * (t1.val - t.val) = -(x.val⁻¹ * |t2.val - t.val|)h1:t.val ≤ t1.valh2:t2.val < t.val⊢ t2.val - t.val < 0negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:x.val⁻¹ * (t1.val - t.val) = -(x.val⁻¹ * -(t2.val - t.val))h1:t.val ≤ t1.valh2:t2.val < t.val⊢ t1 = t2 linarithAll goals completed! 🐙negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:x.val⁻¹ * (t1.val - t.val) = -(x.val⁻¹ * -(t2.val - t.val))h1:t.val ≤ t1.valh2:t2.val < t.val⊢ t1 = t2)] at hnegx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:x.val⁻¹ * (t1.val - t.val) = -(x.val⁻¹ * -(t2.val - t.val))h1:t.val ≤ t1.valh2:t2.val < t.val⊢ t1 = t2
    simp [← mul_neg] at hnegx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh1:t.val ≤ t1.valh2:t2.val < t.valh:t1.val = t2.val⊢ t1 = t2
    extnegx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh1:t.val ≤ t1.valh2:t2.val < t.valh:t1.val = t2.val⊢ t1.val = t2.val
    exact hAll goals completed! 🐙
  ·posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:¬t ≤ t1h2:t ≤ t2⊢ t1 = t2 simp_all [dist, le_def]posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(x.val⁻¹ * |t1.val - t.val|) = x.val⁻¹ * |t2.val - t.val|h1:t1.val < t.valh2:t.val ≤ t2.val⊢ t1 = t2
    rw [abs_of_neg (byx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(x.val⁻¹ * |t1.val - t.val|) = x.val⁻¹ * |t2.val - t.val|h1:t1.val < t.valh2:t.val ≤ t2.val⊢ t1.val - t.val < 0posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(x.val⁻¹ * -(t1.val - t.val)) = x.val⁻¹ * (t2.val - t.val)h1:t1.val < t.valh2:t.val ≤ t2.val⊢ t1 = t2 linarithAll goals completed! 🐙posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(x.val⁻¹ * -(t1.val - t.val)) = x.val⁻¹ * (t2.val - t.val)h1:t1.val < t.valh2:t.val ≤ t2.val⊢ t1 = t2), abs_of_nonneg (byx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(x.val⁻¹ * -(t1.val - t.val)) = x.val⁻¹ * |t2.val - t.val|h1:t1.val < t.valh2:t.val ≤ t2.val⊢ 0 ≤ t2.val - t.valposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(x.val⁻¹ * -(t1.val - t.val)) = x.val⁻¹ * (t2.val - t.val)h1:t1.val < t.valh2:t.val ≤ t2.val⊢ t1 = t2 linarithAll goals completed! 🐙posx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(x.val⁻¹ * -(t1.val - t.val)) = x.val⁻¹ * (t2.val - t.val)h1:t1.val < t.valh2:t.val ≤ t2.val⊢ t1 = t2)] at hposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(x.val⁻¹ * -(t1.val - t.val)) = x.val⁻¹ * (t2.val - t.val)h1:t1.val < t.valh2:t.val ≤ t2.val⊢ t1 = t2
    simp [← mul_neg] at hposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh1:t1.val < t.valh2:t.val ≤ t2.valh:t1.val = t2.val⊢ t1 = t2
    extposx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh1:t1.val < t.valh2:t.val ≤ t2.valh:t1.val = t2.val⊢ t1.val = t2.val
    exact hAll goals completed! 🐙
  ·negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:(if t ≤ t1 then dist x t t1 else -dist x t t1) = if t ≤ t2 then dist x t t2 else -dist x t t2h1:¬t ≤ t1h2:¬t ≤ t2⊢ t1 = t2 simp_all [dist, le_def]negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:|t1.val - t.val| = |t2.val - t.val|h1:t1.val < t.valh2:t2.val < t.val⊢ t1 = t2
    rw [abs_of_neg (byx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:|t1.val - t.val| = |t2.val - t.val|h1:t1.val < t.valh2:t2.val < t.val⊢ t1.val - t.val < 0negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(t1.val - t.val) = -(t2.val - t.val)h1:t1.val < t.valh2:t2.val < t.val⊢ t1 = t2 linarithAll goals completed! 🐙negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(t1.val - t.val) = -(t2.val - t.val)h1:t1.val < t.valh2:t2.val < t.val⊢ t1 = t2), abs_of_neg (byx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(t1.val - t.val) = |t2.val - t.val|h1:t1.val < t.valh2:t2.val < t.val⊢ t2.val - t.val < 0negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(t1.val - t.val) = -(t2.val - t.val)h1:t1.val < t.valh2:t2.val < t.val⊢ t1 = t2 linarithAll goals completed! 🐙negx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(t1.val - t.val) = -(t2.val - t.val)h1:t1.val < t.valh2:t2.val < t.val⊢ t1 = t2)] at hnegx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh:-(t1.val - t.val) = -(t2.val - t.val)h1:t1.val < t.valh2:t2.val < t.val⊢ t1 = t2
    simp at hnegx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh1:t1.val < t.valh2:t2.val < t.valh:t1.val = t2.val⊢ t1 = t2
    extnegx:TimeUnitt:TimeTransMant1:TimeTransMant2:TimeTransManh1:t1.val < t.valh2:t2.val < t.valh:t1.val = t2.val⊢ t1.val = t2.val
    exact hAll goals completed! 🐙

lemma diff_fst_surjective (x : TimeUnit) (t : TimeTransMan) :
    Function.Surjective (diff x · t) := byx:TimeUnitt:TimeTransMan⊢ Function.Surjective fun x_1 => diff x x_1 t
  intro rx:TimeUnitt:TimeTransManr:ℝ⊢ ∃ a, (fun x_1 => diff x x_1 t) a = r
  simp [diff, dist]x:TimeUnitt:TimeTransManr:ℝ⊢ ∃ a, (if t ≤ a then x.val⁻¹ * |a.val - t.val| else -(x.val⁻¹ * |a.val - t.val|)) = r
  use x.1 * r +ᵥ thx:TimeUnitt:TimeTransManr:ℝ⊢ (if t ≤ x.val * r +ᵥ t then x.val⁻¹ * |(x.val * r +ᵥ t).val - t.val| else -(x.val⁻¹ * |(x.val * r +ᵥ t).val - t.val|)) =
  r
  simp [abs_mul]hx:TimeUnitt:TimeTransManr:ℝ⊢ (if t ≤ x.val * r +ᵥ t then x.val⁻¹ * (|x.val| * |r|) else -(x.val⁻¹ * (|x.val| * |r|))) = r
  rw [abs_of_nonneg (le_of_lt x.val_pos)hx:TimeUnitt:TimeTransManr:ℝ⊢ (if t ≤ x.val * r +ᵥ t then x.val⁻¹ * (x.val * |r|) else -(x.val⁻¹ * (x.val * |r|))) = rhx:TimeUnitt:TimeTransManr:ℝ⊢ (if t ≤ x.val * r +ᵥ t then x.val⁻¹ * (x.val * |r|) else -(x.val⁻¹ * (x.val * |r|))) = r]hx:TimeUnitt:TimeTransManr:ℝ⊢ (if t ≤ x.val * r +ᵥ t then x.val⁻¹ * (x.val * |r|) else -(x.val⁻¹ * (x.val * |r|))) = r
  simp only [ne_eq, TimeUnit.val_ne_zero, not_false_eq_true, inv_mul_cancel_left₀]hx:TimeUnitt:TimeTransManr:ℝ⊢ (if t ≤ x.val * r +ᵥ t then |r| else -|r|) = r
  by_cases h : 0 ≤ rposx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ (if t ≤ x.val * r +ᵥ t then |r| else -|r|) = rnegx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ (if t ≤ x.val * r +ᵥ t then |r| else -|r|) = r
  ·posx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ (if t ≤ x.val * r +ᵥ t then |r| else -|r|) = r rw [if_posposx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ |r| = rpos.hcx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ t ≤ x.val * r +ᵥ tposx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ |r| = rpos.hcx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ t ≤ x.val * r +ᵥ t]posx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ |r| = rpos.hcx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ t ≤ x.val * r +ᵥ t
    exact abs_of_nonneg hpos.hcx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ t ≤ x.val * r +ᵥ t
    simp [le_def]pos.hcx:TimeUnitt:TimeTransManr:ℝh:0 ≤ r⊢ 0 ≤ x.val * r
    apply mul_nonneg (le_of_lt x.val_pos) hAll goals completed! 🐙
  ·negx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ (if t ≤ x.val * r +ᵥ t then |r| else -|r|) = r rw [if_negnegx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ -|r| = rneg.hncx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ ¬t ≤ x.val * r +ᵥ tnegx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ -|r| = rneg.hncx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ ¬t ≤ x.val * r +ᵥ t]negx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ -|r| = rneg.hncx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ ¬t ≤ x.val * r +ᵥ t
    rw [abs_of_neg (byx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ r < 0negx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ - -r = rneg.hncx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ ¬t ≤ x.val * r +ᵥ t simpa using hAll goals completed! 🐙negx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ - -r = rneg.hncx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ ¬t ≤ x.val * r +ᵥ t)]negx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ - -r = rneg.hncx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ ¬t ≤ x.val * r +ᵥ t
    simp only [neg_neg]neg.hncx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ ¬t ≤ x.val * r +ᵥ t
    simp [le_def]neg.hncx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ x.val * r < 0
    refine mul_neg_of_pos_of_neg x.val_pos (byx:TimeUnitt:TimeTransManr:ℝh:¬0 ≤ r⊢ r < 0 simpa using hAll goals completed! 🐙)lemma diff_fst_bijective (x : TimeUnit) (t : TimeTransMan) :
    Function.Bijective (diff x · t) :=
  ⟨diff_fst_injective x t, diff_fst_surjective x t⟩

Adding time



lemma addTime_eq_val (x : TimeUnit) (r : ℝ) (t : TimeTransMan) :
    (addTime x r t) = ⟨x.1 * r + t.val⟩ := byx:TimeUnitr:ℝt:TimeTransMan⊢ addTime x r t = { val := x.val * r + t.val }
  apply diff_fst_injective x tx:TimeUnitr:ℝt:TimeTransMan⊢ (fun x_1 => diff x x_1 t) (addTime x r t) = (fun x_1 => diff x x_1 t) { val := x.val * r + t.val }
  change (diff x · t) (Function.invFun ((diff x · t)) r) = _x:TimeUnitr:ℝt:TimeTransMan⊢ (fun x_1 => diff x x_1 t) (Function.invFun (fun x_1 => diff x x_1 t) r) =
  (fun x_1 => diff x x_1 t) { val := x.val * r + t.val }
  rw [Function.rightInverse_invFun (diff_fst_surjective x t)x:TimeUnitr:ℝt:TimeTransMan⊢ r = (fun x_1 => diff x x_1 t) { val := x.val * r + t.val }x:TimeUnitr:ℝt:TimeTransMan⊢ r = (fun x_1 => diff x x_1 t) { val := x.val * r + t.val }]x:TimeUnitr:ℝt:TimeTransMan⊢ r = (fun x_1 => diff x x_1 t) { val := x.val * r + t.val }
  simp [diff_eq_val]All goals completed! 🐙



lemma addTime_val (x : TimeUnit) (r : ℝ) (t : TimeTransMan) :
    (addTime x r t).val = x.1 * r + t.val := byx:TimeUnitr:ℝt:TimeTransMan⊢ (addTime x r t).val = x.val * r + t.val
  rw [addTime_eq_valx:TimeUnitr:ℝt:TimeTransMan⊢ { val := x.val * r + t.val }.val = x.val * r + t.valAll goals completed! 🐙]All goals completed! 🐙

Negation of time around a zero

lemma neg_eq_negMetric (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) :
    neg zero t = negMetric zero x t := byzero:TimeTransManx:TimeUnitt:TimeTransMan⊢ zero.neg t = zero.negMetric x t
  simp [neg, negMetric]zero:TimeTransManx:TimeUnitt:TimeTransMan⊢ addTime default (diff default zero t) zero = addTime x (diff x zero t) zero
  extzero:TimeTransManx:TimeUnitt:TimeTransMan⊢ (addTime default (diff default zero t) zero).val = (addTime x (diff x zero t) zero).val
  simp [addTime_val, diff_eq_val]All goals completed! 🐙

The map from TimeTransMan to Time

              @[simp]
lemma toTime_zero (zero : TimeTransMan) (x : TimeUnit) :
    toTime zero x zero = 0 := byzero:TimeTransManx:TimeUnit⊢ (zero.toTime x) zero = 0
  extzero:TimeTransManx:TimeUnit⊢ ((zero.toTime x) zero).val = Time.val 0
  simp [toTime, diff_eq_val]All goals completed! 🐙@[simp]
lemma toTime_symm_zero_add (zero : TimeTransMan) (x : TimeUnit) :
    (toTime zero x).symm 0 = zero := byzero:TimeTransManx:TimeUnit⊢ (zero.toTime x).symm 0 = zero
  extzero:TimeTransManx:TimeUnit⊢ ((zero.toTime x).symm 0).val = zero.val
  simp [toTime, addTime_val, diff_eq_val]All goals completed! 🐙lemma toTime_val (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) :
    (toTime zero x t).val = diff x t zero := byzero:TimeTransManx:TimeUnitt:TimeTransMan⊢ ((zero.toTime x) t).val = diff x t zero rflAll goals completed! 🐙lemma toTime_symm_val (zero : TimeTransMan) (x : TimeUnit) (r : Time) :
    (toTime zero x).symm r = addTime x r zero := byzero:TimeTransManx:TimeUnitr:Time⊢ (zero.toTime x).symm r = addTime x r.val zero
  extzero:TimeTransManx:TimeUnitr:Time⊢ ((zero.toTime x).symm r).val = (addTime x r.val zero).val
  simp [toTime, addTime_val, diff_eq_val]All goals completed! 🐙@[simp]
lemma toTime_addTime (zero : TimeTransMan) (x : TimeUnit) (r : ℝ) (τ : TimeTransMan) :
    toTime zero x (addTime x r τ) = ⟨r⟩ + toTime zero x τ:= byzero:TimeTransManx:TimeUnitr:ℝτ:TimeTransMan⊢ (zero.toTime x) (addTime x r τ) = { val := r } + (zero.toTime x) τ
  extzero:TimeTransManx:TimeUnitr:ℝτ:TimeTransMan⊢ ((zero.toTime x) (addTime x r τ)).val = ({ val := r } + (zero.toTime x) τ).val
  simp [toTime_val, diff_eq_val, addTime_val]zero:TimeTransManx:TimeUnitr:ℝτ:TimeTransMan⊢ x.val⁻¹ * (x.val * r + τ.val - zero.val) = r + x.val⁻¹ * (τ.val - zero.val)
  field_simpzero:TimeTransManx:TimeUnitr:ℝτ:TimeTransMan⊢ x.val * r + τ.val - zero.val = x.val * r + (τ.val - zero.val)
  ringAll goals completed! 🐙lemma toTime_symm_add (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : Time) :
    (toTime zero x).symm (t1 + t2) = addTime x (diff x ((toTime zero x).symm t1) zero)
      ((toTime zero x).symm t2) := byzero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ (zero.toTime x).symm (t1 + t2) = addTime x (diff x ((zero.toTime x).symm t1) zero) ((zero.toTime x).symm t2)
  extzero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ ((zero.toTime x).symm (t1 + t2)).val = (addTime x (diff x ((zero.toTime x).symm t1) zero) ((zero.toTime x).symm t2)).val
  simp [addTime_val, diff_eq_val, toTime_symm_val]zero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ x.val * (t1.val + t2.val) + zero.val = x.val * t1.val + (x.val * t2.val + zero.val)
  ringAll goals completed! 🐙lemma toTime_symm_add' (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : Time) :
    (toTime zero x).symm (t1 + t2) = addTime x (diff x ((toTime zero x).symm t2) zero)
      ((toTime zero x).symm t1) := byzero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ (zero.toTime x).symm (t1 + t2) = addTime x (diff x ((zero.toTime x).symm t2) zero) ((zero.toTime x).symm t1)
  extzero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ ((zero.toTime x).symm (t1 + t2)).val = (addTime x (diff x ((zero.toTime x).symm t2) zero) ((zero.toTime x).symm t1)).val
  simp [addTime_val, diff_eq_val, toTime_symm_val]zero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ x.val * (t1.val + t2.val) + zero.val = x.val * t2.val + (x.val * t1.val + zero.val)
  ringAll goals completed! 🐙lemma diff_eq_toTime_sub (zero : TimeTransMan) (x : TimeUnit) (t1 t2 : TimeTransMan) :
    diff x t2 t1 = toTime zero x t2 - toTime zero x t1 := byzero:TimeTransManx:TimeUnitt1:TimeTransMant2:TimeTransMan⊢ diff x t2 t1 = ((zero.toTime x) t2).val - ((zero.toTime x) t1).val
  simp [toTime_val, diff_eq_val]zero:TimeTransManx:TimeUnitt1:TimeTransMant2:TimeTransMan⊢ x.val⁻¹ * (t2.val - t1.val) = x.val⁻¹ * (t2.val - zero.val) - x.val⁻¹ * (t1.val - zero.val)
  field_simpzero:TimeTransManx:TimeUnitt1:TimeTransMant2:TimeTransMan⊢ t2.val - t1.val = t2.val - zero.val - (t1.val - zero.val)
  ringAll goals completed! 🐙

lemma toTime_neg (zero : TimeTransMan) (x : TimeUnit) (t : TimeTransMan) :
    (toTime zero x) (neg zero t) = - toTime zero x t := byzero:TimeTransManx:TimeUnitt:TimeTransMan⊢ (zero.toTime x) (zero.neg t) = -(zero.toTime x) t
  rw [neg_eq_negMetric zero xzero:TimeTransManx:TimeUnitt:TimeTransMan⊢ (zero.toTime x) (zero.negMetric x t) = -(zero.toTime x) tzero:TimeTransManx:TimeUnitt:TimeTransMan⊢ (zero.toTime x) (zero.negMetric x t) = -(zero.toTime x) t]zero:TimeTransManx:TimeUnitt:TimeTransMan⊢ (zero.toTime x) (zero.negMetric x t) = -(zero.toTime x) t
  extzero:TimeTransManx:TimeUnitt:TimeTransMan⊢ ((zero.toTime x) (zero.negMetric x t)).val = (-(zero.toTime x) t).val
  simp only [negMetric, diff_eq_val, one_div, toTime_addTime, toTime_zero,
    add_zero, Time.neg_val, toTime_val]zero:TimeTransManx:TimeUnitt:TimeTransMan⊢ x.val⁻¹ * (zero.val - t.val) = -(x.val⁻¹ * (t.val - zero.val))
  ringAll goals completed! 🐙lemma toTime_symm_neg (zero : TimeTransMan) (x : TimeUnit) (t : Time) :
    (toTime zero x).symm (- t) = neg zero ((toTime zero x).symm t) := byzero:TimeTransManx:TimeUnitt:Time⊢ (zero.toTime x).symm (-t) = zero.neg ((zero.toTime x).symm t)
  extzero:TimeTransManx:TimeUnitt:Time⊢ ((zero.toTime x).symm (-t)).val = (zero.neg ((zero.toTime x).symm t)).val
  simp [toTime_symm_val, addTime_val, diff_eq_val, neg, negMetric]All goals completed! 🐙lemma toTime_symm_sub (zero : TimeTransMan) (x : TimeUnit)
    (t1 t2 : Time) : (toTime zero x).symm (t1 - t2) =
      addTime x (diff x zero ((toTime zero x).symm t2))
      ((toTime zero x).symm t1) := byzero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ (zero.toTime x).symm (t1 - t2) = addTime x (diff x zero ((zero.toTime x).symm t2)) ((zero.toTime x).symm t1)
  extzero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ ((zero.toTime x).symm (t1 - t2)).val = (addTime x (diff x zero ((zero.toTime x).symm t2)) ((zero.toTime x).symm t1)).val
  simp [addTime_val, diff_eq_val, toTime_symm_val]zero:TimeTransManx:TimeUnitt1:Timet2:Time⊢ x.val * (t1.val - t2.val) + zero.val = -(x.val * t2.val) + (x.val * t1.val + zero.val)
  ringAll goals completed! 🐙

The time manifold with a transitive action of ℝ