pith. sign in
module module high

IndisputableMonolith.Gravity.RotationILG

show as:
view Lean formalization →

This module defines the ILG-enhanced rotation velocity satisfying the fixed-point equation v squared equals w sub t of r comma v times G M sub b over r. It integrates the Rotation system with ILG gravity enhancements in the Recognition Science framework. Galaxy dynamics researchers would cite it when modeling rotation curves without dark matter. The module organizes definitions and existence results around the imported components with no internal proofs.

claimThe ILG-enhanced rotation velocity $v$ satisfies the fixed-point equation $v^2 = w_t(r, v) · (G M_b / r)$.

background

The module sits in the Gravity domain and imports the RS time quantum τ₀ = 1 tick from Constants. The Rotation import supplies the gravitational constant G together with the enclosed mass function Menc. The ILG import supplies the core gravity enhancements that modify the standard rotation setup. The local theoretical setting combines these imports to produce velocity solutions obeying the fixed-point relation stated in the module comment.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the ILG-enhanced rotation model that supports sibling results including solution_exists and SPARC_mismatch_falsifier. It fills the gap between the base Rotation system and ILG gravity by enforcing the fixed-point velocity equation inside the Recognition Science treatment of galactic dynamics.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (3)