phi_neg_44
plain-language theorem explainer
Defines the rung-44 forcing scale φ^{-44} as a real constant from the golden-ratio base. Cosmologists cite it as the common sub-leading amplitude shared by the RS dark-energy w(z) discriminator and the baryon asymmetry η_B. The body is a one-line power of Constants.phi.
Claim. Let $\varphi$ be the golden ratio. Define the real constant $\varphi^{-44} := \varphi^{(-44)}$.
background
Track 4.C of the RS cosmology program asks for a falsifiable dark-energy equation of state that differs from ΛCDM's strict $w=-1$ only at a sub-leading scale fixed by the φ-ladder. The module supplies a structural linear placeholder $w_{\mathrm{RS}}(z)=-1+\varphi^{-44}\cdot z$ whose deviation amplitude is exactly this constant.
The same integer rung appears in baryogenesis: $\eta_B=\varphi^{-44}$ via the PhiRungLadder assignment eta_B_rung_val = -44. Thus $\varphi^{-44}$ is the shared forcing scale linking early-universe asymmetry to late-time dark-energy drift. Numerically $\varphi^{-44}\approx 6.38\times 10^{-10}$.
Upstream, Constants.phi is the unique self-similar fixed point forced by the Recognition Composition Law (T5–T6). The definition simply evaluates the integer power of that constant.
proof idea
Pure definition: evaluate Constants.phi raised to the integer exponent $-44$. No lemmas, no tactics; the declaration is noncomputable only because real exponentiation is noncomputable in Lean.
why it matters
This constant is the algebraic discriminator of Track 4.C. Downstream it appears in w_RS_linear, the positivity lemma phi_neg_44_pos, the falsifier threshold $\varphi^{-44}\cdot z$, the named bands at $z=1/2$ and $z=1$, the master cert DarkEnergyWofZStructuralCert, and the one-statement theorem that packages ΛCDM match at $z=0$ with strict excess at positive redshift.
It ties the dark-energy prediction to the same rung that fixes baryogenesis, so a single φ-ladder integer controls both. The module leaves the true FPT cosmic Z-aging $z$-dependence as future work; the linear placeholder is only a non-vacuous witness that the amplitude is $\varphi^{-44}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.