Encyclopedia Gravity Gravity Parameterization Bridge Accel
ARTICLE 4 claims 4 theorems
Gravity Parameterization Bridge Accel
A short definition that turns circular motion into a bridge between two ways of writing gravity, and the exact algebra that holds them together.
The acceleration bridge
In classical mechanics, an object moving in a circle at constant speed v and radius r has a centripetal acceleration a = v²/r, always directed toward the center. This is one of the first formulas a physics student meets, and it is purely kinematic: it follows from the geometry of circular motion, not from any particular force law. The Recognition Science library formalizes this definition as the function accel, which takes speed and radius as real numbers and returns v²/r.
From this starting point, the library derives a small family of exact identities that connect acceleration to time. The orbital period for one full revolution is T_dyn = 2πr/v. The library proves that a·T_dyn² = 4π²r, a relation that holds whenever both v and r are nonzero. It also defines a characteristic time T₀ = 2π√(r₀/a₀) built from a length scale r₀ and an acceleration scale a₀, and proves that T₀² = 4π²(r₀/a₀) when r₀ is nonnegative and a₀ is positive.
The central result is a bridge identity: for circular motion, (T_dyn/T₀)² = (a₀/a)·(r/r₀). This says that a ratio of times equals a product of ratios of accelerations and radii. The library proves this in both directions, and also proves a special case at the characteristic radius r = r₀: raising the acceleration ratio to a power α is exactly equivalent to raising the time ratio to the power 2α. Conversely, a time exponent α corresponds to an acceleration exponent α/2. These are pure algebra, fully proven in the machine-checked library of formal theorems, with no unproved assumptions.
In Recognition Science, this bridge matters because it lets a model written in acceleration space be rewritten in time space without changing its content. The identities are exact, not approximations. But they are also narrow: they describe circular motion only, they require nonzero speed and radius, and they say nothing about what causes the acceleration. The bridge connects two parameterizations of the same kinematics; it does not derive gravity, does not introduce new physics, and does not claim that any particular force law follows from these definitions.
THEOREM accel · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- Circular-orbit centripetal acceleration from speed `v` and radius `r`. -/
def accel (v r : ℝ) : ℝ := v^2 / r
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
What this page does not claim
This answer does not claim that accel or the bridge identities derive any force law or predict any gravitational effect. This answer does not claim that the identities hold outside circular motion or when speed or radius is zero. This answer does not claim that the framework assigns physical meaning to the scales r₀ and a₀ beyond their role in the algebra.
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 force law, if any, does the Recognition Science framework derive for circular orbits from its cost function?
- How do these exact kinematic identities connect to the framework's treatment of weight forms in gravity models?
- What physical interpretation does the framework give to the characteristic radius r₀ and acceleration scale a₀?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM accel · IndisputableMonolith/Gravity/ParameterizationBridge.lean
/-- Circular-orbit centripetal acceleration from speed `v` and radius `r`. -/ def accel (v r : ℝ) : ℝ := v^2 / rIn classical mechanics, an object moving in a circle at constant speed v and radius r has a centripetal acceleration a = v²/r, always directed toward the center. accel · IndisputableMonolith/Gravity/ParameterizationBridge.leanTHEOREM 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 library proves that a·T_dyn² = 4π²r, a relation that holds whenever both v and r are nonzero. 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]The central result is a bridge identity: for circular motion, (T_dyn/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 the characteristic radius r = r₀: raising the acceleration ratio to a power α is exactly equivalent to raising the time ratio to the power 2α. accel_power_eq_time_power_at_r_eq_r0 · IndisputableMonolith/Gravity/ParameterizationBridge.lean