Gravity Parameterization Bridge Accel Ratio Eq Time Ratio Sq Mul R0 Over R

The acceleration-time bridge

For an object moving in a circle of radius r at speed v, two elementary quantities are always linked: the centripetal acceleration a = v²/r and the orbital period T_dyn = 2πr/v, the time for one full revolution. The framework's library, a machine-checked collection of formal theorems, proves an exact identity connecting the ratio of two such accelerations to the ratio of two such times. In plain symbols, the theorem accel_ratio_eq_time_ratio_sq_mul_r0_over_r states that (a0/a) = (T_dyn/T0)² · (r0/r), where a0 and r0 are a reference acceleration and radius, and T0 = 2π√(r0/a0) is a characteristic time built from them.

This identity is a pure consequence of the definitions of a and T_dyn; it is not a new physical law. It is the algebraic bridge that lets a model written in terms of acceleration ratios be rewritten in terms of time ratios, and vice versa. For example, if a model uses (a0/a)^α as its core term, the theorem shows that at the special radius r = r0, this is exactly equal to (T_dyn/T0)^(2α). The factor of 2 in the exponent comes from the fact that T_dyn is proportional to √(r/a), so squaring the time ratio recovers the acceleration ratio.

The theorem's proof is fully formalized in the framework's library, with no gaps. It requires only that the speeds and radii are positive, so the ratios are well-defined. The identity holds for any circular motion, regardless of the force that causes it, because it is derived solely from the kinematic definitions of acceleration and period.

What the theorem does not claim is more important than what it does. It does not state that any particular gravitational model, such as Modified Newtonian Dynamics or a specific dark matter profile, is correct. It does not derive the value of the gravitational constant G or any other physical constant. It does not even assert that real orbits are circular; it is a statement about the mathematical relationship between two quantities defined for circular motion. The theorem is a tool for translating between two equivalent parameterizations, not a claim about which parameterization describes nature.

/-- Rearranged bridge:
\[
\frac{a_0}{a} = \left(\frac{T_{\rm dyn}}{T_0}\right)^2\left(\frac{r_0}{r}\right).
\]
-/
theorem accel_ratio_eq_time_ratio_sq_mul_r0_over_r
    (v r a0 r0 : ℝ) (hv : 0 < v) (hr : 0 < r) (ha0 : 0 < a0) (hr0 : 0 < r0) :
    let a := accel v r
    let T := Tdyn v r
    let Tref := T0 r0 a0
    (a0 / a) = (T / Tref)^2 * (r0 / r) := by
  -- Algebraic rearrangement of time_ratio_sq_eq_accel_ratio_mul_r_ratio
  intro a T Tref
  have hbridge :
      (T / Tref)^2 = (a0 / a) * (r / r0) := by
    simpa [a, T, Tref] using
      time_ratio_sq_eq_accel_ratio_mul_r_ratio (v := v) (r := r) (a0 := a0) (r0 := r0) hv hr ha0 hr0

  have hr_ne : r ≠ 0 := ne_of_gt hr
  have hr0_ne : r0 ≠ 0 := ne_of_gt hr0

  have hcancel : (r / r0) * (r0 / r) = (1 : ℝ) := by
    field_simp [hr_ne, hr0_ne]

  -- Multiply both sides of the bridge by `r0/r` and simplify.
  have hmul := congrArg (fun x => x * (r0 / r)) hbridge
  have : (T / Tref)^2 * (r0 / r) = a0 / a := by
    -- Reassociate and cancel `(r/r0) * (r0/r) = 1`.
    simpa [mul_assoc, hcancel] using hmul

  exact this.symm

/-- Core identity: \(a\,T_{\rm dyn}^2 = 4\pi^2 r\). -/
theorem accel_mul_Tdyn_sq (v r : ℝ) (hv : v ≠ 0) (hr : r ≠ 0) :
    accel v r * (Tdyn v r)^2 = 4 * (Real.pi ^ 2) * r := by
  unfold accel Tdyn
  field_simp [hv, hr]
  ring

/-- Rearranged bridge:
\[
\frac{a_0}{a} = \left(\frac{T_{\rm dyn}}{T_0}\right)^2\left(\frac{r_0}{r}\right).
\]
-/
theorem accel_ratio_eq_time_ratio_sq_mul_r0_over_r
    (v r a0 r0 : ℝ) (hv : 0 < v) (hr : 0 < r) (ha0 : 0 < a0) (hr0 : 0 < r0) :
    let a := accel v r
    let T := Tdyn v r
    let Tref := T0 r0 a0
    (a0 / a) = (T / Tref)^2 * (r0 / r) := by
  -- Algebraic rearrangement of time_ratio_sq_eq_accel_ratio_mul_r_ratio
  intro a T Tref
  have hbridge :
      (T / Tref)^2 = (a0 / a) * (r / r0) := by
    simpa [a, T, Tref] using
      time_ratio_sq_eq_accel_ratio_mul_r_ratio (v := v) (r := r) (a0 := a0) (r0 := r0) hv hr ha0 hr0

  have hr_ne : r ≠ 0 := ne_of_gt hr
  have hr0_ne : r0 ≠ 0 := ne_of_gt hr0

  have hcancel : (r / r0) * (r0 / r) = (1 : ℝ) := by
    field_simp [hr_ne, hr0_ne]

  -- Multiply both sides of the bridge by `r0/r` and simplify.
  have hmul := congrArg (fun x => x * (r0 / r)) hbridge
  have : (T / Tref)^2 * (r0 / r) = a0 / a := by
    -- Reassociate and cancel `(r/r0) * (r0/r) = 1`.
    simpa [mul_assoc, hcancel] using hmul

  exact this.symm

What this page does not claim

The theorem does not assert that any particular gravitational model is correct. The theorem does not derive the value of the gravitational constant G. The theorem does not claim that real orbits are circular.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/ParameterizationBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: