IndisputableMonolith.Gravity.ILGRealExponentEnhancement
This module defines the ILG radial weight for arbitrary real exponent α and proves its core analytic properties. Researchers modeling asymptotic galactic dynamics or extending the Recognition Science gravity chain would cite these results to handle non-integer exponents. The module consists of a base definition followed by direct applications of real exponentiation rules and limit arguments imported from Mathlib.
claimThe ILG radial weight with real exponent is $w(R) = 1 + C (R/r_0)^α$ for $α ∈ ℝ$, $R > 0$. Theorems establish that $α > 0$ implies $w > 1$, that the map is strictly increasing in $R$, that the squared velocity term dominates the Newtonian contribution at large radii, and that the enhancement is unbounded as $R → ∞$.
background
In the Recognition Science framework the Information-Limited Gravity (ILG) model augments Newtonian gravity by a radial weight that encodes information bounds. The upstream module ILGAsymptoticEnhancement supplies the structural theorems for Phase D9 of the SPARC pre-registration paper, where the weight takes the form $w(R) = 1 + C (R/r_0)^α$ and the exponent is initially treated in restricted cases. This module removes the restriction on α, allowing any real value while preserving the same functional shape.
proof idea
This is a definition module. It opens with the core definition w_real that accepts α : ℝ without sign assumptions. The remaining declarations are short theorems that apply the standard lemmas on real powers (positivity, monotonicity, and asymptotic dominance) to obtain enhancement_real_pos, enhancement_real_strict_mono, ilg_real_velocity_sq_dominates_newtonian, and enhancement_real_unbounded.
why it matters in Recognition Science
The module completes the real-exponent case required for flexible ILG modeling inside the broader gravity hierarchy. It directly supports the asymptotic enhancement theorems of Phase D9 and supplies the analytic foundation for any downstream result that needs to vary the exponent continuously rather than restrict it to integers or positives.
scope and limits
- Does not assume α > 0 in the base definition.
- Does not derive a preferred numerical value for α.
- Does not include observational fitting or parameter estimation.
- Does not treat relativistic or time-dependent extensions.
- Does not prove that this weight is the unique solution to the ILG functional equation.