beta_growth_pos
plain-language theorem explainer
The theorem establishes that the ILG growth parameter β(k) = (2/3) φ^{-3/2} (k τ₀)^{-α} is strictly positive for positive real k and τ₀. Cosmologists modeling enhanced structure formation in ILG-modified cosmologies cite this to guarantee D(a,k) > a relative to the GR baseline. The proof is a direct term-mode reduction that unfolds the definition and applies mul_pos together with rpow_pos_of_pos on the positive factors.
Claim. For all real $k > 0$ and fundamental tick duration $τ_0 > 0$, the ILG growth kernel satisfies $β(k, τ_0) > 0$, where $β(k, τ_0) = (2/3) φ^{-3/2} (k τ_0)^{-α}$ and $α = α_{lock} ≈ 0.191$.
background
The module formalizes the ILG-modified linear growth factor from the Dark-Energy and Hubble-Tension papers. Core definitions are D(a,k) = a (1 + β(k) a^α)^{1/(1+α)}, β(k) = (2/3) φ^{-3/2} (k τ₀)^{-α}, and f(a,k) = 1 + [α/(1+α)] β a^α / (1 + β a^α), with α = alphaLock. The fundamental tick τ₀ is imported from Constants as the duration of one tick in RS-native units (c=1, ħ=φ^{-5}). Upstream results include the definition of beta_growth itself and the positivity of φ from the forcing chain (T5 J-uniqueness).
proof idea
The term proof unfolds beta_growth, then applies mul_pos to the product of the constant factor (2/3) φ^{-3/2} and the power term. The first factor is shown positive by norm_num on 2/3 together with rpow_pos_of_pos on φ (using phi_pos). The second factor is shown positive by rpow_pos_of_pos applied to the product k τ₀ (using the hypotheses hk and ht).
why it matters
This positivity is the base fact feeding D_growth_ge_a, D_growth_pos, f_growth_gt_one, and the GrowthFactorCert structure that packages the ILG enhancement claims. It directly supports the paper statement that ILG produces D > a and f > 1 relative to GR matter domination. The result closes the positivity interface required by the Recognition Science constants (phi, alphaLock) derived from the eight-tick octave and RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.