phi_neg_44_pos
plain-language theorem explainer
The rung-44 scale φ^{-44} is strictly positive. Cosmologists working the structural RS dark-energy discriminator cite this to guarantee that the linear placeholder w(z) = -1 + φ^{-44} z lies strictly above ΛCDM's constant w = -1 at any positive redshift. The proof unfolds the definition and applies Mathlib positivity of integer powers of a positive base.
Claim. Let $\varphi > 1$ be the golden-ratio fixed point. Then $0 < \varphi^{-44}$.
background
Track 4.C of the quantum-gravity master plan asks for a falsifiable dark-energy equation of state w(z) that differs at sub-leading order from ΛCDM's strict w = -1. This module supplies the algebraic discriminator: the deviation scale is the rung-44 factor φ^{-44} (the same scale that appears as the baryogenesis η_B = φ^{-44} on the φ-rung ladder).
Here φ is the self-similar fixed point forced by T6 of the Recognition forcing chain, with φ > 0 already available from the constants layer. The definition phi_neg_44 packages the integer power φ^{-44} ≈ 6.38 × 10^{-10}. Positivity of that constant is the elementary arithmetic fact needed before any comparison of w profiles can be stated.
The module is honest that the linear placeholder w_RS_linear(z) := -1 + φ^{-44} · z is only a structural witness, not the physical RS cosmic-aging kernel (which is antitone and of amplitude J(φ) ≈ 0.118 today). Positivity of the slope is still required for the discriminator inequalities that follow.
proof idea
One-line term proof after unfolding. Expand phi_neg_44 to the integer power φ^{-44}, then apply Mathlib's zpow_pos to the already-proved fact phi_pos (φ > 0). The exponent is irrelevant once the base is positive, so the goal 0 < φ^{-44} closes immediately.
why it matters
Without 0 < φ^{-44}, the structural placeholder w_RS_linear cannot be shown to exceed ΛCDM at positive z, and the master cert darkEnergyWofZStructuralCert has no positive deviation magnitude to quote. The same constant is the baryogenesis scale η_B = φ^{-44} on the φ-rung ladder, so the positivity lemma is shared infrastructure between cosmology Track 4.C and the baryon-asymmetry story.
Downstream siblings (w_RS_linear_distinct_from_LCDM_at_positive_z, w_RS_linear_deviation_magnitude, falsifierThreshold_pos) all need a strictly positive coefficient in front of z. The module status is structural theorem with zero sorry; this lemma is the first arithmetic brick under that claim. The physically correct RS kernel w(z) = -1 + J(φ)/(1+z) remains future work; the present result only underwrites the linear witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.