pith. sign in
module module moderate

IndisputableMonolith.Gravity.ParameterizationBridge

show as:
view Lean formalization →

The ParameterizationBridge module supplies algebraic identities connecting centripetal acceleration in circular orbits to ratios of dynamic time T_dyn and reference time T_0. Researchers formalizing gravity models in Recognition Science cite it when linking the fine-structure constant alpha to those time ratios. The module consists of direct definitions of quantities such as accel together with their multiplicative and ratio relations.

claimDefines centripetal acceleration $a = v^2/r$ and establishes relations including $a imes T_{ m dyn}^2$, $T_0^2$, $(T_{ m dyn}/T_0)^2 = (a/a_0) imes (r_0/r)$, and the corresponding power identities at reference radius $r_0$.

background

The module belongs to the Gravity facade, which re-exports Rotation (Newtonian identities $v^2 = GM/r$), ILG (time-kernel and weight functions), DerivedFactors (HSB suppression from SevenBeatViolation), and ParameterizationBridge itself. It introduces the explicit bridge from alpha to $T_{ m dyn}/T_0$ ratios. Core objects are accel (circular-orbit centripetal acceleration from speed $v$ and radius $r$), Tdyn, T0, and the listed multiplicative lemmas.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module is imported by IndisputableMonolith.Gravity, the facade collecting all gravity formalizations. It supplies the parameterization step that links alpha to $T_{ m dyn}/T_0$ ratios, completing the bridge required by the Recognition Science gravity layer.

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)