Encyclopedia Gravity Gravity Parameterization Bridge Time Ratio Sq Eq Accel Ratio Mul R Ratio

ARTICLE 4 claims 4 theorems

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

A single algebraic identity shows that for circular motion, the square of the time ratio equals the acceleration ratio times the radius ratio, linking two ways of describing gravity.

Verify this page

The kinematic bridge

For an object moving in a circle at constant speed, two classical quantities are always related. The centripetal acceleration a is the square of the speed v divided by the radius r, so a = v²/r. The dynamical time T_dyn, the time for one full revolution, is the circumference divided by the speed, so T_dyn = 2πr/v. From these two definitions alone, a simple identity follows: a times T_dyn² equals 4π²r. This is not a law of gravity; it is a fact about circular motion that holds for any speed and radius, as long as both are nonzero.

The Recognition Science library formalizes this classical fact and a more general version of it. The theorem time_ratio_sq_eq_accel_ratio_mul_r_ratio (a machine-checked statement in the framework's library of formal theorems) proves that for circular motion, the square of the ratio of the dynamical time to a characteristic time T₀ equals the ratio of a reference acceleration a₀ to the actual acceleration a, multiplied by the ratio of the radius r to a reference radius r₀. In symbols: (T_dyn/T₀)² = (a₀/a)(r/r₀). The characteristic time T₀ is defined as 2π√(r₀/a₀), built from a chosen length scale r₀ and acceleration scale a₀. The theorem requires all speeds, radii, and accelerations to be positive, and it is proved with no unproved assumptions.

This identity is called a bridge because it lets a model written in terms of acceleration ratios be rewritten in terms of time ratios, and vice versa. At the special radius where r equals r₀, the bridge simplifies further: (a₀/a) raised to the power α equals (T_dyn/T₀) raised to the power 2α. That means an exponent on an acceleration ratio corresponds to twice that exponent on a time ratio, at that characteristic radius. The library also proves the reverse direction: a time exponent α maps to an acceleration exponent α/2. These exponent mappings are exact algebraic consequences of the definitions, not new physical assumptions.

What this theorem does not claim is just as important. It does not assert that any particular force law, such as Newton's inverse-square law, follows from these definitions. The identity holds for any circular motion, regardless of what causes the acceleration. It does not claim that the characteristic time T₀ is the actual orbital period of any real system; T₀ is a constructed scale, not a measured quantity. And it does not claim that the exponent mapping applies away from the characteristic radius r = r₀; the simplified power relation is proved only at that special point. The theorem is a kinematic fact about circular motion, precisely stated and verified, that lets one parameterization of a gravity model be translated into another.

THEOREM time_ratio_sq_eq_accel_ratio_mul_r_ratio · IndisputableMonolith/Gravity/ParameterizationBridge.lean
time_ratio_sq_eq_accel_ratio_mul_r_ratio · IndisputableMonolith/Gravity/ParameterizationBridge.lean:58 
/-- **Bridge identity (exact):**
\[
\left(\frac{T_{\rm dyn}}{T_0}\right)^2 = \left(\frac{a_0}{a}\right)\left(\frac{r}{r_0}\right)
\]
for circular motion with \(a=v^2/r\) and \(T_{\rm dyn}=2\pi r/v\).

This is the fundamental kinematic identity underlying the acceleration↔time parameterization.
-/
theorem time_ratio_sq_eq_accel_ratio_mul_r_ratio
    (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
    (T / Tref)^2 = (a0 / a) * (r / r0) := by
  -- Direct algebraic verification
  intro a T Tref
  dsimp [a, T, Tref]
  have hv0 : v ≠ 0 := ne_of_gt hv
  have hr0' : r ≠ 0 := ne_of_gt hr
  have ha0_ne : a0 ≠ 0 := ne_of_gt ha0
  have hr0_ne : r0 ≠ 0 := ne_of_gt hr0

  have ha : accel v r ≠ 0 := by
    unfold accel
    exact div_ne_zero (pow_ne_zero 2 hv0) hr0'

  -- Expand the square of a ratio as a ratio of squares.
  rw [div_pow (Tdyn v r) (T0 r0 a0) 2]

  -- Use the pre-proved square identities for `Tdyn` and `T0`.
  have hT_sq : (Tdyn v r)^2 = (4 * (Real.pi ^ 2) * r) / accel v r := by
    have h := accel_mul_Tdyn_sq (v := v) (r := r) hv0 hr0'
    apply (eq_div_iff ha).2
    -- Commute multiplication to match the target.
    simpa [mul_comm, mul_left_comm, mul_assoc] using h

  have hT0_sq : (T0 r0 a0)^2 = 4 * (Real.pi ^ 2) * (r0 / a0) :=
    T0_sq r0 a0 (le_of_lt hr0) ha0

  rw [hT_sq, hT0_sq]
  -- Clear denominators and finish by ring normalization.
  field_simp [ha, ha0_ne, hr0_ne]
THEOREM accel_mul_Tdyn_sq · IndisputableMonolith/Gravity/ParameterizationBridge.lean
accel_mul_Tdyn_sq · IndisputableMonolith/Gravity/ParameterizationBridge.lean:41 
/-- 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
THEOREM accel_power_eq_time_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean
accel_power_eq_time_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean:133 
/-- **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
THEOREM time_power_eq_accel_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean
time_power_eq_accel_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean:174 
/-- **Exponent bridge (time→acceleration form):** at the characteristic radius \(r=r_0\),
\[
\left(\frac{T_{\rm dyn}}{T_0}\right)^{\alpha}
= \left(\frac{a_0}{a}\right)^{\alpha/2}.
\]

This is the exact mapping when the exponent \(\alpha\) is interpreted as the
**time-exponent** (as in a time-kernel), and one rewrites the model in acceleration space.
-/
theorem time_power_eq_accel_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
    (T / Tref) ^ α = (a0 / a) ^ (α / 2) := by
  intro a T Tref
  -- Use the already-proved form with exponent α/2
  have h := accel_power_eq_time_power_at_r_eq_r0 v r0 a0 (α / 2) hv hr0 ha0
  -- h: (a0/a)^(α/2) = (T/Tref)^(2*(α/2)) = (T/Tref)^α
  have : 2 * (α / 2) = α := by ring
  simp only [this] at h
  exact h.symm

What this page does not claim

The theorem does not derive any particular force law, such as Newton's inverse-square law, from the definitions. The theorem does not claim that the characteristic time T₀ is the actual orbital period of any real system. The theorem does not claim that the exponent mapping applies away from the characteristic radius r = r₀.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND