module module high

`IndisputableMonolith.Gravity.ILGAsymptoticEnhancement`

This module defines the locked ILG amplitude as the abstract positive constant C = φ^{-3/2}. It isolates this value to support asymptotic enhancement results in the gravity domain while remaining independent of Real.rpow. The module structure supplies the amplitude lock before dependent modules extend the facts to the real exponent α = 1 - 1/φ. Researchers on ILG velocity profiles cite it for the fixed amplitude in the phi-ladder setting.

claimThe locked ILG amplitude satisfies $C = \phi^{-3/2}$ with $C > 0$, treated as an abstract positive constant.

background

Recognition Science places this module in the gravity domain, where the phi-ladder supplies mass and enhancement factors via the self-similar fixed point φ from T6. The module introduces C_lock as the locked amplitude φ^{-3/2}, represented by a positive abstract constant to defer dependence on real exponentiation. It imports the Constants module whose sole documented fact is the RS time quantum τ₀ = 1 tick.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the amplitude lock that feeds IndisputableMonolith.Gravity.ILGRealExponentEnhancement. That downstream module states it extends the natural-power envelope to the locked real exponent α = 1 − 1/φ ∈ (0,1) via Real.rpow, proving four structural facts about radial enhancement. The present module therefore closes the qualitative step before the real-exponent treatment in phase D9.

scope and limits

Does not compute or approximate the numerical value of φ^{-3/2}.
Does not prove any enhancement positivity or monotonicity statements.
Does not depend on or invoke Real.rpow.
Does not address BTFR slope identities or velocity-squared dominance.
Does not treat the real-exponent case α = 1 − 1/φ.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.ILGRealExponentEnhancement module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (12)

def C_lock L46
theorem C_lock_pos L48
def w_radial L57
theorem enhancement_pos L59
theorem enhancement_above_one L67
theorem enhancement_strict_mono L75
theorem enhancement_unbounded L95
theorem ilg_velocity_sq_dominates_newtonian L147
def BTFRSlopeIdentity L173
theorem btfr_slope_identity_iff L177
structure ILGAsymptoticEnhancementCert L191
theorem ilgAsymptoticEnhancementCert_holds L206