pith. sign in
module module high

IndisputableMonolith.Gravity.ParameterizationBridge

show as:
view Lean formalization →

ParameterizationBridge links the fine-structure constant alpha to T_dyn over T_0 ratios while defining centripetal acceleration and related orbital identities. Gravity formalizers working on rotation curves or ILG time kernels cite these bridges. The module consists of a set of definitions and equalities for acceleration, time scales, and power relations at reference radii.

claimDefines centripetal acceleration $a = v^2/r$ together with dynamic time $T_{ m dyn}$, reference time $T_0$, and identities such as $a imes T_{ m dyn}^2$, time-ratio squares, and power equalities at $r = r_0$, bridging to the parameter $\\alpha$.

background

The Gravity module facade re-exports Newtonian rotation identities (v² = GM/r), ILG time-kernel functions, HSB suppression factors, and this ParameterizationBridge. The bridge supplies the concrete link from alpha to the ratio T_dyn/T_0 that appears in orbital and time-power relations. All objects are expressed in the Recognition Science native units where c = 1.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module is imported by IndisputableMonolith.Gravity, the top-level facade that assembles Rotation, ILG, DerivedFactors, and ParameterizationBridge. It supplies the alpha-to-time-ratio bridge required by the ILG component of the Recognition Science gravity formalization.

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)