pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Gravity.ParameterizationBridge

show as:
view Lean formalization →

The ParameterizationBridge module defines centripetal acceleration for circular orbits and the algebraic identities that relate acceleration ratios to squared T_dyn over T_0 ratios scaled by radius ratios. Gravity modelers in Recognition Science cite it to connect the fine-structure constant α to dynamic time parameters. The module consists of direct definitions and equalities with no inductive proofs.

claim$a(v,r)=v^2/r$, together with the bridge relations $(T_0/T_0)^2=(a/a_0)(r/r_0)$, $a/a_0=(T_0/T_0)^2(r_0/r)$, and the corresponding power-law identities at reference radius $r=r_0$.

background

The Gravity module re-exports Rotation for Newtonian rotation curves, ILG for information-limited time kernels, DerivedFactors for HSB suppression, and ParameterizationBridge to link α to T_dyn/T_0 ratios. This module introduces the centripetal acceleration accel(v,r) and the time-ratio identities that allow parameterization of gravitational dynamics through these time scales in RS-native units where c=1.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the IndisputableMonolith.Gravity facade, which re-exports it to connect Rotation and ILG components. It supplies the explicit algebraic link from α to T_dyn/T_0 ratios required for gravity parameterization in the Recognition Science framework.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (9)