T0

formal source

  36T_0 = 2\pi\sqrt{r_0/a_0}.
  37\]
  38-/
  39def T0 (r0 a0 : ℝ) : ℝ := 2 * Real.pi * Real.sqrt (r0 / a0)
  40
  41/-- Core identity: \(a\,T_{\rm dyn}^2 = 4\pi^2 r\). -/
  42theorem accel_mul_Tdyn_sq (v r : ℝ) (hv : v ≠ 0) (hr : r ≠ 0) :
  43    accel v r * (Tdyn v r)^2 = 4 * (Real.pi ^ 2) * r := by
  44  unfold accel Tdyn
  45  field_simp [hv, hr]
  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