Pith. sign in
module module high

IndisputableMonolith.Gravity.ILGRealExponentEnhancement

show as:
view Lean formalization →

This module defines the ILG radial weight allowing any real exponent α, without positivity built into the definition. Researchers extending asymptotic gravity modifications in the v07 verifier would reference the w_real construction and its monotonicity lemmas. The module consists of a core definition plus short lemmas establishing positivity, strict increase, and dominance over Newtonian gravity.

claim$w_{\rm real}(R;\alpha,C,r_0)=1+C(R/r_0)^\alpha$ for $\alpha\in\mathbb{R}$. The module establishes that the weight remains positive for $C>0$, is strictly monotone in $R$ when $\alpha>0$, and produces unbounded enhancement as $R\to\infty$.

background

The upstream module ILGAsymptoticEnhancement states that the Information-Limited Gravity radial weight takes the form $w(R)=1+C(R/r_0)^\alpha$ and supplies the structural theorems of Phase D9 in papers/RS_PhiLocked_SPARC_Prereg.md. This module removes any positivity hypothesis on the exponent from the definition itself. Sibling declarations then record the resulting positivity, monotonicity, and velocity-dominance statements for unrestricted real α.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module extends the ILG asymptotic enhancement framework to real exponents, directly supporting the structural theorems listed in the parent ILGAsymptoticEnhancement module. It fills the requirement that the radial weight definition itself impose no sign restriction on α, thereby preparing the ground for later gravity-domain results that may invoke arbitrary real powers.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)