IndisputableMonolith.Gravity.ParameterizationBridge
Bridge module linking circular-orbit centripetal acceleration to dynamical-time ratios used when parameterizing Information-Limited Gravity. Defines $a=v^2/r$, $T_{\mathrm{dyn}}$, and $T_0$, then records the elementary ratio and power identities that convert $(T_{\mathrm{dyn}}/T_0)$ into $a/a_0$ (and conversely). Gravity and ILG developers cite it when wiring $\alpha$ to observable rotation-curve scales. Content is definitions plus short algebraic rearrangements.
claimOn a circular orbit, centripetal acceleration is $a=v^2/r$. With dynamical time $T_{\mathrm{dyn}}$ and reference $T_0$ at radius $r_0$, the module states $(T_{\mathrm{dyn}}/T_0)^2=(a/a_0)(r_0/r)$, the inverted form $a/a_0=(T_{\mathrm{dyn}}/T_0)^2(r_0/r)^{-1}$, and the equalities of acceleration and time powers when $r=r_0$.
background
Recognition Science gravity (ILG) expresses its information-limited weight through a dimensionless parameter often written via ratios of dynamical times. The Gravity facade lists this module as the bridge that links $\alpha$ to $T_{\mathrm{dyn}}/T_0$ ratios, so classical kinematics must be available in Lean before those ratios can be substituted into ILG kernels.
Centripetal acceleration on a circular orbit is the Newtonian $a=v^2/r$. Dynamical time $T_{\mathrm{dyn}}$ is the orbital (or free-fall) timescale at radius $r$; $T_0$ is the same quantity evaluated at a fixed reference radius $r_0$. Because period scales as $r/v$ while $a$ scales as $v^2/r$, the squared time ratio is proportional to the acceleration ratio times a pure geometric factor $r_0/r$.
Sibling declarations package exactly those identities: products $a,T_{\mathrm{dyn}}^2$, squares $T_0^2$, and the two directions of the ratio map, plus the collapse of acceleration-power and time-power when $r=r_0$.
proof idea
Definition-and-identity module, not a deep proof development. Accelerations and times are introduced as plain defs from $v$ and $r$. The ratio lemmas are short algebraic rewrites: multiply or divide the defining relations $a=v^2/r$ and $T\propto r/v$, cancel, and rearrange factors of $r_0/r$. At $r=r_0$ the geometric prefactor is one, so acceleration powers and time powers coincide by substitution. No analysis or external gravity theorems are required.
why it matters in Recognition Science
The Gravity facade re-exports this module explicitly as "Links $\alpha$ to $T_{\mathrm{dyn}}/T_0$ ratios," alongside Rotation, ILG time-kernels, and DerivedFactors. Downstream ILG and rotation-curve formalizations therefore import these identities rather than re-deriving Newtonian circular-orbit kinematics each time an $\alpha$-parameterization is matched to an acceleration scale. Within the broader RS gravity stack, that keeps the classical bridge thin and reusable while the information-limited weight and HSB suppression live in sibling modules.
scope and limits
- Does not derive ILG field equations or the $\alpha$ weight function.
- Does not treat non-circular orbits or pressure-supported systems.
- Does not fix $G$, masses, or numerical galactic parameters.
- Does not claim empirical rotation-curve fits or dark-matter constraints.
- Does not address relativistic or cosmological corrections.