pith. machine review for the scientific record. sign in
theorem proved tactic proof

T0_sq

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  49theorem T0_sq (r0 a0 : ℝ) (hr0 : 0 ≤ r0) (ha0 : 0 < a0) :
  50    (T0 r0 a0)^2 = 4 * (Real.pi ^ 2) * (r0 / a0) := by

proof body

Tactic-mode proof.

  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-/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.