Encyclopedia Gravity Gravity Parameterization Bridge
ARTICLE 4 claims 4 theorems
Gravity Parameterization Bridge
A set of exact algebraic identities connects how gravity models are written in acceleration space to how they are written in time space, with no approximation.
The kinematic bridge
In classical mechanics, a body moving in a circle of radius r with speed v has a centripetal acceleration a = v²/r. Its dynamical time, the period of one full revolution, is Tdyn = 2πr/v. These two quantities are not independent. The product of the acceleration and the square of the period equals 4π² times the radius: a·Tdyn² = 4π²r. This identity is as old as circular motion itself, but it becomes a powerful bookkeeping tool when a theory has two natural languages for writing its laws.
One language is acceleration space: a model states how acceleration depends on radius, often as a ratio (a₀/a) raised to some exponent α. The other language is time space: the same model states how the orbital period depends on radius, often as a ratio (Tdyn/T₀) raised to an exponent. The bridge is the exact relation between these two ratios. At the characteristic radius where r equals r₀, the identity takes a clean form: (Tdyn/T₀)² = (a₀/a)·(r/r₀). At that special radius, the radius ratio is 1, and the bridge collapses to a pure exponent mapping: (a₀/a)^α = (Tdyn/T₀)^(2α). An exponent of α in acceleration space corresponds to an exponent of 2α in time space, and conversely a time exponent of α maps to an acceleration exponent of α/2.
In Recognition Science, the framework treats gravity as a recognition process and writes its weight forms in either parameterization. The bridge matters because it shows the two forms are not competing theories; they are the same kinematic content expressed in different coordinates. The module in the framework's machine-checked library of formal theorems proves these identities as exact algebraic statements, not as approximations. The proofs require only that speeds, radii, and acceleration scales be positive, and they hold for any circular orbit, with no assumption about the force law that produces the motion.
The practical consequence is a translation rule. If a researcher writes a gravity model as a power law in acceleration ratio, the bridge tells them exactly what exponent to use when rewriting it as a power law in time ratio, and vice versa. This is not a physical discovery about what gravity is; it is a kinematic fact about how circular motion is described. The bridge is what makes the two parameterizations interchangeable, and it is the precise statement behind the informal idea that acceleration-based and time-based gravity models are equivalent.
THEOREM accel_mul_Tdyn_sq · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- 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 time_ratio_sq_eq_accel_ratio_mul_r_ratio · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- **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_power_eq_time_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- **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
/-- **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 bridge does not derive any specific force law or gravity model. The identities hold only for circular motion, not for general orbits. The module does not establish that acceleration-based and time-based gravity models are physically equivalent beyond kinematics.
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:
- How does the bridge generalize to elliptical orbits, where the period and radius are not constant?
- What physical content, if any, is lost when a gravity model is rewritten from acceleration space to time space?
- Does the bridge impose any constraint on the allowed exponents in a recognition-based gravity model?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM accel_mul_Tdyn_sq · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- 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] ringThe product of the acceleration and the square of the period equals 4π² times the radius: a·T<sub>dyn</sub>² = 4π²r. accel_mul_Tdyn_sq · IndisputableMonolith/Gravity/ParameterizationBridge.leanTHEOREM time_ratio_sq_eq_accel_ratio_mul_r_ratio · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- **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]At the characteristic radius where r equals r₀, the identity takes a clean form: (T<sub>dyn</sub>/T₀)² = (a₀/a)·(r/r₀). time_ratio_sq_eq_accel_ratio_mul_r_ratio · IndisputableMonolith/Gravity/ParameterizationBridge.leanTHEOREM accel_power_eq_time_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- **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_castAt that special radius, the radius ratio is 1, and the bridge collapses to a pure exponent mapping: (a₀/a)^α = (T<sub>dyn</sub>/T₀)^(2α). accel_power_eq_time_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.leanTHEOREM time_power_eq_accel_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- **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.symmConversely a time exponent of α maps to an acceleration exponent of α/2. time_power_eq_accel_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean