beta_growth
Defines the ILG growth kernel parameter β(k) as (2/3) φ^{-3/2} (k τ₀)^{-α} with α = alphaLock ≈ 0.191. Cosmologists constructing modified growth models for dark energy and Hubble tension would cite this when building the scale-dependent D(a,k). The definition is a direct algebraic expression using the phi-ladder prefactor and the locked exponent.
claim$β(k) = (2/3) φ^{-3/2} (k τ_0)^{-α}$ where $α = (1 - 1/φ)/2$.
background
The module formalizes the ILG-modified growth factor D(a,k) and growth rate f(a,k) from the Dark-Energy and Hubble-Tension papers. Core relations are D(a,k) = a (1 + β(k) a^α)^{1/(1+α)} and f(a,k) = 1 + [α/(1+α)] β a^α / (1 + β a^α), with α = alphaLock and τ₀ the fundamental tick. alphaLock is the canonical locked fine-structure constant (1 − 1/φ)/2. tau0 supplies the RS-native time unit, drawn from Constants and Compat layers.
proof idea
Direct definition as the algebraic product (2/3) * phi^(-3/2) * (k * tau0)^(-alphaLock).
why it matters in Recognition Science
Supplies the β(k) parameter required by downstream D_growth, f_growth, and GrowthFactorCert. It encodes the CPM paper prefactor C = φ^{-3/2} inside the Recognition Science constants, enabling the claims D > a and f > 1 that distinguish ILG from GR. The definition closes the kernel step in the ILG growth chain.
scope and limits
- Does not prove positivity of β for positive k and τ₀.
- Does not derive the form of α or the prefactor from the forcing chain.
- Does not evaluate β at specific cosmological scales.
- Does not address higher-order corrections beyond linear growth.
formal statement (Lean)
41noncomputable def beta_growth (k tau0 : ℝ) : ℝ :=
proof body
Definition body.
42 (2 / 3) * phi ^ (-(3/2 : ℝ)) * (k * tau0) ^ (-alphaLock)
43
44/-- β is positive for positive k and τ₀. -/