Encyclopedia Gravity Gravity Parameterization Bridge Accel Power Eq Time Power At R Eq R0
ARTICLE 4 claims 4 theorems
Gravity Parameterization Bridge Accel Power Eq Time Power At R Eq R0
At one special radius, acceleration and time exponents in gravity models are the same quantity written two ways.
The exponent bridge
In circular motion, a body moving at speed v around a circle of radius r has a centripetal acceleration a = v²/r. The time for one full orbit, called the dynamical time Tdyn, is the circumference divided by the speed: Tdyn = 2πr/v. These two formulas are the standard kinematics of circular orbits, and they are related by the identity a·Tdyn² = 4π²r, which follows from substituting one into the other. This identity is a theorem in the framework's machine-checked library of formal theorems, proved for all nonzero speeds and radii.
Now introduce a second length scale r₀ and a second acceleration scale a₀, and build a characteristic time T₀ = 2π√(r₀/a₀). This T₀ is the time it would take to complete one orbit at radius r₀ with acceleration a₀. The bridge identity compares the two times and the two accelerations: (Tdyn/T₀)² = (a₀/a)·(r/r₀). At the special radius r = r₀, the radius ratio becomes 1, and the identity simplifies to (Tdyn/T₀)² = a₀/a. Raising both sides to a power α gives (a₀/a)α = (Tdyn/T₀)2α. This is the declaration accel_power_eq_time_power_at_r_eq_r0: it states that an exponent α on the acceleration ratio is exactly equivalent to an exponent 2α on the time ratio, at the characteristic radius.
The declaration is a pure algebraic identity, not a physical law. It does not say that gravity actually follows any particular power law, nor that orbits are circular, nor that any specific value of α is correct. It only says that if a model is written with an acceleration exponent and a time exponent, those two exponents are the same quantity at r = r₀, differing by a factor of two. The converse form, time_power_eq_accel_power_at_r_eq_r0, states the same mapping in reverse: an exponent α on the time ratio equals an exponent α/2 on the acceleration ratio. Both are proved in the framework's library as exact algebraic identities for positive speeds, radii, and accelerations.
In Recognition Science, this bridge is the precise link between two ways of parameterizing gravity models: one that writes weights as powers of acceleration ratios, and one that writes them as powers of time ratios. The framework proves the bridge so that a model expressed in one parameterization can be translated into the other without approximation, at the characteristic radius. What the bridge does not do is choose the exponent α, justify the use of circular orbits, or derive the acceleration scale a₀ from deeper principles. Those remain separate modeling choices and open targets, not consequences of this identity.
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 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 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
This identity does not assert that gravity follows any particular power law or that any value of α is physically correct. The bridge does not derive the acceleration scale a₀ or the radius r₀ from deeper principles; those are modeling inputs. The identity holds at the characteristic radius r = r₀ only, not at arbitrary radii.
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:
- What physical principle, if any, selects the characteristic radius r₀ and acceleration scale a₀ for a real gravitational system?
- How does the bridge identity generalize when orbits are not circular, so that a and T<sub>dyn</sub> are not related by the simple circular formulas?
- Does the framework derive the exponent α from the forcing chain, or is α always a free modeling parameter?
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 identity a·T<sub>dyn</sub>² = 4π²r follows from the definitions of acceleration and dynamical time for circular motion. accel_mul_Tdyn_sq · 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 the characteristic radius r = r₀, the bridge identity simplifies to (T<sub>dyn</sub>/T₀)² = a₀/a. accel_power_eq_time_power_at_r_eq_r0 · 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_castAn exponent α on the acceleration ratio is exactly equivalent to an exponent 2α on the time ratio at r = r₀. 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.symmThe converse form states that an exponent α on the time ratio equals an exponent α/2 on the acceleration ratio. time_power_eq_accel_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean