Gravity Parameterization Bridge Tdyn

The dynamical time

For a body moving in a circle, two basic quantities describe the motion: the acceleration toward the center, a = v²/r, and the time for one full revolution, T = 2πr/v. The second of these, Tdyn, is the dynamical time. It is the period of a circular orbit, measured in seconds, and it depends only on the speed and the radius. A faster body completes the circle sooner; a larger circle takes longer. This is classical kinematics, and it holds for any circular motion, from a stone on a string to a planet around a star.

The useful fact is that these two quantities are not independent. Multiply acceleration by the square of the dynamical time and you get exactly 4π² times the radius: a·Tdyn² = 4π²r. This identity, proved in the framework's machine-checked library of formal theorems, is the bridge between describing an orbit by its acceleration and describing it by its time. A related construction, the characteristic time T0 = 2π√(r0/a0), plays the same role when a length scale and an acceleration scale are chosen as reference points. The square of T0 equals 4π²(r0/a0), and the ratio of the two times obeys (Tdyn/T0)² = (a0/a)(r/r0).

In Recognition Science, this bridge matters because weight forms in the framework can be parameterized either by acceleration or by time. The library proves that at the characteristic radius r = r0, an acceleration exponent α maps exactly to a time exponent 2α, and conversely a time exponent α maps to an acceleration exponent α/2. These exponent bridges are the precise algebraic statements behind the informal practice of rewriting models between the two parameterizations. The theorems are fully proven in the machine-checked library, with no gaps.

What Tdyn does not claim is physics beyond kinematics. It is a definition, not a law of gravity. It does not say what force produces the circular motion, does not require the orbit to be stable, and does not apply to elliptical orbits without modification. The framework's library proves the algebraic identities that relate acceleration and time for circular motion; it does not derive the inverse-square law or any particular gravitational field from these definitions. The bridge is exact, but it is a bridge over a narrow strait: it connects two ways of writing the same circular motion, and it leaves the dynamics that cause the motion entirely open.

/-- Orbital (dynamical) time for circular motion (one full revolution). -/
def Tdyn (v r : ℝ) : ℝ := 2 * Real.pi * r / v

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

/-- **Exponent bridge (canonical special case):** at the characteristic radius \(r=r_0\),
\[
\left(\frac{a_0}{a}\right)^\alpha = \left(\frac{T_{\rm dyn}}{T_0}\right)^{2\alpha}.
\]

This is the exact statement behind the common "acceleration exponent vs time exponent" mapping:
if a model is written with \((a_0/a)^{\alpha_{\rm acc}}\), the corresponding exponent on
the time-ratio base is \(2\alpha_{\rm acc}\) (at \(r=r_0\)).
-/
theorem accel_power_eq_time_power_at_r_eq_r0
    (v r0 a0 α : ℝ) (hv : 0 < v) (hr0 : 0 < r0) (ha0 : 0 < a0) :
    let a := accel v r0
    let T := Tdyn v r0
    let Tref := T0 r0 a0
    (a0 / a) ^ α = (T / Tref) ^ ((2 : ℝ) * α) := by
  intro a T Tref
  -- At r = r0, from the bridge: (T/Tref)^2 = a0/a
  -- Thus (a0/a)^α = ((T/Tref)^2)^α = (T/Tref)^(2α)
  have h : (T / Tref)^2 = a0 / a := by
    have hbridge := time_ratio_sq_eq_accel_ratio_mul_r_ratio v r0 a0 r0 hv hr0 ha0 hr0
    have hr00 : r0 ≠ 0 := ne_of_gt hr0
    simp only [div_self hr00, mul_one] at hbridge
    exact hbridge
  rw [← h]
  have hT_pos : 0 < T := by
    unfold T Tdyn
    have h2pi : 0 < (2 : ℝ) * Real.pi := by nlinarith [Real.pi_pos]
    exact div_pos (mul_pos h2pi hr0) hv
  have hTref_pos : 0 < Tref := by
    unfold Tref T0
    have hpos : 0 < r0 / a0 := div_pos hr0 ha0
    have hsqrt : 0 < Real.sqrt (r0 / a0) := Real.sqrt_pos.mpr hpos
    have h2pi : 0 < (2 : ℝ) * Real.pi := by nlinarith [Real.pi_pos]
    exact mul_pos h2pi hsqrt
  have hratio_pos : 0 < T / Tref := div_pos hT_pos hTref_pos
  have hratio_nonneg : 0 ≤ T / Tref := le_of_lt hratio_pos
  -- ((T/Tref)^2)^α = (T/Tref)^(2*α)
  rw [← Real.rpow_natCast (T / Tref) 2]
  rw [← Real.rpow_mul hratio_nonneg]
  norm_cast

What this page does not claim

Tdyn does not describe elliptical orbits or non-uniform motion. The definition of Tdyn does not imply any particular force law or gravitational field. The exponent bridge theorems do not hold away from the characteristic radius r = r0.

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: