pith. sign in
module module high

IndisputableMonolith.Gravity

show as:
view Lean formalization →

The Gravity module aggregates the Information-Limited Gravity (ILG) weight kernel with rotation curves, dynamical-time parameterization, and derived morphology factors. Researchers modeling galactic dynamics or lab propulsion within the Recognition Science framework would cite it. The module structures its content by importing four submodules that together supply the gravitational relations without internal proofs.

claimThe module supplies the ILG weight kernel relating enclosed mass $M_ {enc}$ to acceleration $a = v^2/r$, dynamical time $T_{dyn} = 2π r/v$, characteristic time $T_0 = 2π √(r_0/a_0)$, morphology factor $ξ$, and radial factor $n(r)$, with gravitational constant $G$.

background

This module organizes the gravity sector of Recognition Science by importing four submodules. The ParameterizationBridge submodule formalizes the exact algebraic identities that relate circular-orbit acceleration $a = v^2/r$, orbital/dynamical time $T_{dyn} = 2π r/v$, and the common characteristic time $T_0 = 2π √(r_0/a_0)$. The DerivedFactors submodule attempts to derive the ξ (morphology) and n(r) (radial) factors from first principles, specifically using the logic of SevenBeatViolation and ScaleGate saturation, addressing HSB overprediction in the ILG kernel. The Rotation submodule supplies the gravitational constant G and enclosed mass function Menc, while ILG provides the core weight kernel.

proof idea

This is an aggregation module with no internal proofs. It imports ILG for the weight kernel, Rotation for the mass function, ParameterizationBridge for the time-acceleration identities, and DerivedFactors for the morphology and radial corrections derived from scale gates.

why it matters in Recognition Science

This module supplies the gravitational components to the Flight.GravityBridge, which connects the ILG weight kernel from Gravity.ILG to the Flight/Propulsion model. It addresses key questions on dynamical time for rotating lab devices and fills the gravity sector in the Recognition Science chain.

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.