pith. sign in
module module high

IndisputableMonolith.Gravity.ILGGrowthFactor

show as:
view Lean formalization →

The module defines the ILG growth kernel parameter β(k) = (2/3) φ^{-3/2} (k τ_0)^{-α} with α = (1-1/φ)/2 in the Recognition Science gravity setting. Cosmologists computing structure growth within RS models would cite these definitions and their supporting lemmas. The module supplies core definitions for β, D, and f growth factors plus lemmas on positivity and limiting behavior.

claimThe ILG growth kernel parameter satisfies $β(k) = (2/3) φ^{-3/2} (k τ_0)^{-α}$ where $α = (1 - φ^{-1})/2$ and $τ_0$ denotes the RS time quantum.

background

Recognition Science builds gravity from the unified forcing chain with φ as self-similar fixed point and τ_0 = 1 tick as fundamental time. This module imports the Constants module for τ_0 and introduces the growth kernel β(k) whose prefactor φ^{-3/2} matches the CPM paper constant C. It further defines D_growth as the integrated growth factor, f_growth as its logarithmic derivative, and GrowthFactorCert as the certifying structure.

proof idea

This is a definition module. It states the explicit formula for β(k) and the auxiliary growth functions, then proves positivity via beta_growth_pos and D_growth_pos together with limit statements via D_growth_gr_limit and f_growth_gr_limit.

why it matters in Recognition Science

The module supplies the growth kernel β(k) required for perturbation evolution in ILG gravity. It directly supports GrowthFactorCert and links to the phi-ladder constants with α derived from φ. The construction ties the prefactor to earlier CPM results and places the growth calculation inside the RS framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)