accel

formal source

  26noncomputable section
  27
  28/-- Circular-orbit centripetal acceleration from speed `v` and radius `r`. -/
  29def accel (v r : ℝ) : ℝ := v^2 / r
  30
  31/-- Orbital (dynamical) time for circular motion (one full revolution). -/
  32def Tdyn (v r : ℝ) : ℝ := 2 * Real.pi * r / v
  33
  34/-- Characteristic dynamical time constructed from a length scale `r0` and acceleration scale `a0`:
  35\[
  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\[