Pith. sign in
module module high

IndisputableMonolith.Gravity

show as:
view Lean formalization →

Gravity module aggregates submodules deriving morphology ξ and radial n(r) factors from scale gates, formalizing acceleration-time identities, and defining rotation with G and Menc. Researchers extending ILG to flight models cite it for the weight kernel. The module is a container of four imports with no central theorem.

claimModule organizing identities $a = v^2/r$, $T_{ m dyn} = 2\pi r/v$, $T_0 = 2\pi \sqrt{r_0/a_0}$, morphology factor $\xi$, radial factor $n(r)$, and rotation system with $G$ and enclosed mass $M_{\rm enc}$.

background

The Gravity module imports four submodules to support Information-Limited Gravity. DerivedFactors derives the morphology factor ξ and radial factor n(r) from SevenBeatViolation and ScaleGate saturation to correct HSB overprediction in the ILG kernel. ParameterizationBridge supplies the algebraic bridge between circular acceleration a = v²/r, dynamical time T_dyn = 2π r/v, and characteristic time T0 = 2π √(r0/a0). Rotation supplies the system with gravitational constant G and enclosed mass function Menc.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the ILG weight kernel and derived factors to Flight.GravityBridge, which connects Gravity.ILG to the Flight/Propulsion model and addresses T_dyn for rotating lab devices.

scope and limits

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.