pith. sign in
module module high

IndisputableMonolith.Gravity

show as:
view Lean formalization →

Gravity module assembles the ILG kernel with rotation curves using enclosed mass Menc, the parameterization bridge linking acceleration a = v²/r to dynamical time T_dyn, and derived morphology ξ plus radial n(r) factors. A physicist modeling galactic rotation or modified gravity would cite it to connect Recognition Science constants to observable data. The module consists of four targeted imports that organize these components without internal proofs.

claimThe module organizes the ILG weight kernel relating circular acceleration $a = v^2/r$ to dynamical time $T_{dyn} = 2π r/v$, the morphology factor $ξ$ and radial factor $n(r)$ derived via SevenBeatViolation and ScaleGate, and the enclosed-mass rotation system with constant $G$.

background

Gravity imports four submodules whose doc-comments define the local setting. 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 identities connecting $a = v^2/r$, $T_{dyn} = 2π r/v$, and the characteristic time $T_0 = 2π √(r_0/a_0)$. Rotation supplies the gravitational constant G together with the enclosed-mass function Menc. ILG supplies the core Information-Limited Gravity kernel. The module therefore sits inside the Recognition Science derivation of gravity from the single functional equation, with J-uniqueness and the phi-ladder as upstream structure.

proof idea

This is a definition module with no proofs. It structures the gravity formalization solely by importing DerivedFactors, ILG, ParameterizationBridge, and Rotation, thereby exposing the ILG kernel and its supporting algebraic identities to downstream modules.

why it matters in Recognition Science

The module feeds IndisputableMonolith.Flight.GravityBridge, which connects the ILG weight kernel from Gravity.ILG to the Flight/Propulsion model and addresses the question of T_dyn for a rotating lab device. It therefore supplies the gravity component required for extending the Recognition framework (T0-T8 chain, RCL, phi-ladder) into flight and propulsion calculations.

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.