module module high

`IndisputableMonolith.Gravity.ILGAsymptoticEnhancement`

Module defines the locked ILG amplitude as the abstract positive constant C = φ^{-3/2} to keep all proofs independent of Real.rpow. It supplies the basic positivity, strict monotonicity, unboundedness, and Newtonian dominance properties for the radial enhancement function together with the BTFR slope identity. Researchers extending the ILG model to the real exponent α = 1 - 1/φ cite this module for the qualitative envelope. The module consists entirely of definitions and one-line elementary lemmas.

claimThe locked ILG amplitude is the positive abstract constant $C = φ^{-3/2}$. The radial enhancement function $E(r)$ satisfies $E(r) > 0$, $E(r) > 1$ for $r$ large, is strictly increasing, and is unbounded; moreover $w_{radial}$ dominates the Newtonian term and the BTFR slope identity holds.

background

This module sits inside the Recognition Science gravity development and imports only the fundamental time quantum τ₀ = 1 tick from Constants. It introduces the locked amplitude C_lock = φ^{-3/2} together with the radial weight w_radial and the enhancement function whose properties are recorded as enhancement_pos, enhancement_above_one, enhancement_strict_mono, enhancement_unbounded, and ilg_velocity_sq_dominates_newtonian. The BTFRSlopeIdentity and its equivalence btfr_slope_identity_iff are also defined here, as is the certification object ILGAsymptoticEnhancementCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the qualitative envelope and structural facts that the downstream module IndisputableMonolith.Gravity.ILGRealExponentEnhancement extends to the locked real exponent α = 1 − 1/φ via Real.rpow. It thereby completes the natural-power case required for Phase D9 of the ILG development and feeds directly into the real-exponent structural theorems.

scope and limits

Does not evaluate C numerically or via Real.rpow.
Does not treat time-dependent or quantum corrections.
Does not derive the value of C from the forcing chain.
Does not address non-radial or higher-dimensional cases.

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