`ReachN`

definition

show as: view math explainer →

module: IndisputableMonolith.LightCone.StepBounds
domain: LightCone
line: 13 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.LightCone.StepBounds on GitHub at line 13.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.