phi_pow_44_lower
plain-language theorem explainer
The golden ratio to the 44th power exceeds 1.5×10⁹. Cosmologists certifying the RS baryon-to-photon interval use this lower bound when turning φ^44 bounds into an upper bound on φ^{-44}. The proof rewrites via the Fibonacci closed form and finishes by nonlinear arithmetic from φ>1.61.
Claim. Let $\varphi=(1+\sqrt{5})/2$. Then $\varphi^{44}>1.5\times 10^{9}$.
background
This module certifies the Recognition Science interval for the baryon-to-photon ratio: $\varphi^{-44}\in(5.5\times 10^{-10},7.5\times 10^{-10})$, which contains the Planck 2018 value $\eta_B\approx 6.1\times 10^{-10}$. The integer 44 is structural: $44=4\times 11$, the product of the flip-count on axis 0 and the torsion gap $\Delta\tau_{12}$, the same 44 that appears in the RS formula for $\alpha^{-1}$.
Powers of $\varphi$ obey the Fibonacci identity $\varphi^n=F_n\varphi+F_{n-1}$. The sibling lemma records the concrete case $\varphi^{44}=701408733,\varphi+433494437$. A constants lemma supplies the tight lower bound $\varphi>1.61$ used here.
proof idea
One short tactic proof. Rewrite the goal with the Fibonacci identity $\varphi^{44}=701408733,\varphi+433494437$. Introduce the hypothesis $\varphi>1.61$ from the constants library. Discharge the resulting linear inequality by nlinarith (the affine form in $\varphi$ is strictly above $1.5\times 10^9$ once $\varphi>1.61$).
why it matters
This is the first of the four numerical legs of the $\eta_B$ interval certificate. Downstream, the reciprocal bound $\varphi^{-44}<7.5\times 10^{-10}$ invokes it directly: invert $\varphi^{44}>1.5\times 10^9$ and compare to $7.5\times 10^{-10}$. Together with the matching upper bound on $\varphi^{44}$, it pins $\varphi^{-44}$ inside the observational window.
In the broader framework the exponent 44 is not free: it is the same structural integer that governs the fine-structure formula, linking baryon asymmetry to the chirality–torsion product. The result is fully proved (no sorry) and closes the lower half of the $\varphi^{44}$ sandwich used by the master certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.