IndisputableMonolith.LightCone.StepBounds

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace LightCone
   6
   7variable {α : Type}
   8
   9-- Minimal local Kinematics/ReachN for WIP to avoid external dependency
  10namespace Local
  11structure Kinematics (α : Type) where
  12  step : α → α → Prop
  13inductive ReachN {α} (K : Kinematics α) : Nat → α → α → Prop
  14| zero {x} : ReachN K 0 x x
  15| succ {n x y z} : ReachN K n x y → K.step y z → ReachN K (n+1) x z
  16end Local
  17
  18structure StepBounds (K : Local.Kinematics α)
  19    (U : IndisputableMonolith.Constants.RSUnits)
  20    (time rad : α → ℝ) : Prop where
  21  step_time : ∀ {y z}, K.step y z → time z = time y + U.tau0
  22  step_rad  : ∀ {y z}, K.step y z → rad z ≤ rad y + U.ell0
  23
  24namespace StepBounds
  25
  26variable {K : Local.Kinematics α}
  27variable {U : IndisputableMonolith.Constants.RSUnits}
  28variable {time rad : α → ℝ}
  29
  30lemma reach_time_eq
  31  (H : StepBounds K U time rad) :
  32  ∀ {n x y}, Local.ReachN K n x y → time y = time x + (n : ℝ) * U.tau0 := by
  33  intro n x y h
  34  induction h with
  35  | zero => simp
  36  | @succ n x y z hxy hyz ih =>
  37      have ht := H.step_time hyz
  38      calc
  39        time z = time y + U.tau0 := ht
  40        _ = (time x + (n : ℝ) * U.tau0) + U.tau0 := by simpa [ih]
  41        _ = time x + ((n : ℝ) * U.tau0 + U.tau0) := by simp [add_comm, add_left_comm, add_assoc]
  42        _ = time x + (((n : ℝ) + 1) * U.tau0) := by
  43              have : (n : ℝ) * U.tau0 + U.tau0 = ((n : ℝ) + 1) * U.tau0 := by
  44                calc
  45                  (n : ℝ) * U.tau0 + U.tau0
  46                      = (n : ℝ) * U.tau0 + 1 * U.tau0 := by simpa [one_mul]
  47                  _ = ((n : ℝ) + 1) * U.tau0 := by simpa [add_mul, one_mul]
  48              simp [this]
  49        _ = time x + ((Nat.succ n : ℝ) * U.tau0) := by
  50              simpa [Nat.cast_add, Nat.cast_one]
  51
  52lemma reach_rad_le
  53  (H : StepBounds K U time rad) :
  54  ∀ {n x y}, Local.ReachN K n x y → rad y ≤ rad x + (n : ℝ) * U.ell0 := by
  55  intro n x y h
  56  induction h with
  57  | zero => simp
  58  | @succ n x y z hxy hyz ih =>
  59      have hr := H.step_rad hyz
  60      calc
  61        rad z ≤ rad y + U.ell0 := hr
  62        _ ≤ (rad x + (n : ℝ) * U.ell0) + U.ell0 := by
  63              simpa using (add_le_add_left ih U.ell0)
  64        _ = rad x + ((n : ℝ) * U.ell0 + U.ell0) := by simp [add_comm, add_left_comm, add_assoc]
  65        _ = rad x + (((n : ℝ) + 1) * U.ell0) := by
  66              have : (n : ℝ) * U.ell0 + U.ell0 = ((n : ℝ) + 1) * U.ell0 := by
  67                calc
  68                  (n : ℝ) * U.ell0 + U.ell0
  69                      = (n : ℝ) * U.ell0 + 1 * U.ell0 := by simpa [one_mul]
  70                  _ = ((n : ℝ) + 1) * U.ell0 := by simpa [add_mul, one_mul]
  71              simp [this]
  72        _ = rad x + ((Nat.succ n : ℝ) * U.ell0) := by
  73              simpa [Nat.cast_add, Nat.cast_one]
  74
  75lemma cone_bound
  76  (H : StepBounds K U time rad)
  77  {n x y} (h : Local.ReachN K n x y) :
  78  rad y - rad x ≤ U.c * (time y - time x) := by
  79  have ht := H.reach_time_eq (K:=K) (U:=U) (time:=time) (rad:=rad) h
  80  have hr := H.reach_rad_le  (K:=K) (U:=U) (time:=time) (rad:=rad) h
  81  have hτ : time y - time x = (n : ℝ) * U.tau0 := by
  82    have := congrArg (fun t => t - time x) ht
  83    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this
  84  have hℓ : rad y - rad x ≤ (n : ℝ) * U.ell0 := by
  85    have := hr
  86    -- rearrange ≤ to a difference inequality
  87    have := sub_le_iff_le_add'.mpr this
  88    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
  89  -- In minimal RSUnits, ell0 = c * tau0 is available as the supplied field
  90  have hcτ : U.ell0 = U.c * U.tau0 := by simpa using (U.c_ell0_tau0).symm
  91  simpa [hτ, hcτ, mul_left_comm, mul_assoc] using hℓ
  92
  93/-- Saturation lemma restated: equality holds when each step exactly reaches its bounds. -/
  94lemma cone_bound_saturates
  95  (H : StepBounds K U time rad)
  96  (ht : ∀ {y z}, K.step y z → time z = time y + U.tau0)
  97  (hr : ∀ {y z}, K.step y z → rad z = rad y + U.ell0)
  98  {n x y} (h : Local.ReachN K n x y) :
  99  rad y - rad x = U.c * (time y - time x) := by
 100  have hineq := cone_bound (K:=K) (U:=U) (time:=time) (rad:=rad) H h
 101  have ht' : time y - time x = (n : ℝ) * U.tau0 := by
 102    have := H.reach_time_eq (K:=K) (U:=U) (time:=time) (rad:=rad) h
 103    have := congrArg (fun t => t - time x) this
 104    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using this
 105  have hr' : rad y - rad x = (n : ℝ) * U.ell0 := by
 106    induction h with
 107    | zero => simp
 108    | @succ n x y z hxy hyz ih =>
 109        have hineq_y : rad y - rad x ≤ U.c * (time y - time x) := H.cone_bound hxy
 110        have ht_y : time y - time x = (n : ℝ) * U.tau0 := by
 111          have := H.reach_time_eq hxy
 112          have := congrArg (fun t => t - time x) this
 113          simp [sub_eq_add_neg, add_comm, add_left_comm] at this
 114          exact this
 115        have ih_applied := ih hineq_y ht_y
 116        have hz := hr hyz
 117        calc
 118          rad z - rad x = (rad y + U.ell0) - rad x := by rw [hz]
 119          _ = (rad y - rad x) + U.ell0 := by ring
 120          _ = (n : ℝ) * U.ell0 + U.ell0 := by rw [ih_applied]
 121          _ = ((n : ℝ) + 1) * U.ell0 := by ring
 122          _ = ((Nat.succ n : ℝ)) * U.ell0 := by simp [Nat.cast_add, Nat.cast_one]
 123  have hcτ : U.ell0 = U.c * U.tau0 := by simpa using (U.c_ell0_tau0).symm
 124  calc
 125    rad y - rad x = (n : ℝ) * U.ell0 := hr'
 126    _ = (n : ℝ) * (U.c * U.tau0) := by rw [hcτ]
 127    _ = U.c * ((n : ℝ) * U.tau0) := by ring
 128    _ = U.c * (time y - time x) := by rw [ht']
 129
 130end StepBounds
 131end LightCone
 132end IndisputableMonolith
 133