T0_sq

formal source

  46  ring
  47
  48/-- Square of the characteristic time: \(T_0^2 = 4\pi^2 (r_0/a_0)\). -/
  49theorem T0_sq (r0 a0 : ℝ) (hr0 : 0 ≤ r0) (ha0 : 0 < a0) :
  50    (T0 r0 a0)^2 = 4 * (Real.pi ^ 2) * (r0 / a0) := by
  51  unfold T0
  52  have hnonneg : 0 ≤ r0 / a0 := div_nonneg hr0 (le_of_lt ha0)
  53  have hsq : Real.sqrt (r0 / a0) ^ 2 = r0 / a0 := Real.sq_sqrt hnonneg
  54  calc (2 * Real.pi * Real.sqrt (r0 / a0))^2
  55      = (2 * Real.pi)^2 * (Real.sqrt (r0 / a0))^2 := by ring
  56    _ = 4 * Real.pi^2 * (r0 / a0) := by rw [hsq]; ring
  57
  58/-- **Bridge identity (exact):**
  59\[
  60\left(\frac{T_{\rm dyn}}{T_0}\right)^2 = \left(\frac{a_0}{a}\right)\left(\frac{r}{r_0}\right)
  61\]
  62for circular motion with \(a=v^2/r\) and \(T_{\rm dyn}=2\pi r/v\).
  63
  64This is the fundamental kinematic identity underlying the acceleration↔time parameterization.
  65-/
  66theorem time_ratio_sq_eq_accel_ratio_mul_r_ratio
  67    (v r a0 r0 : ℝ) (hv : 0 < v) (hr : 0 < r) (ha0 : 0 < a0) (hr0 : 0 < r0) :
  68    let a := accel v r
  69    let T := Tdyn v r
  70    let Tref := T0 r0 a0
  71    (T / Tref)^2 = (a0 / a) * (r / r0) := by
  72  -- Direct algebraic verification
  73  intro a T Tref
  74  dsimp [a, T, Tref]
  75  have hv0 : v ≠ 0 := ne_of_gt hv
  76  have hr0' : r ≠ 0 := ne_of_gt hr
  77  have ha0_ne : a0 ≠ 0 := ne_of_gt ha0
  78  have hr0_ne : r0 ≠ 0 := ne_of_gt hr0
  79