phi_pow_neg44_lower
plain-language theorem explainer
The golden ratio satisfies φ^{-44} > 5.5×10^{-10}. Cosmologists citing the RS baryon-to-photon interval use this as the certified lower edge. The proof inverts the already-proved upper bound φ^{44} < 1.6×10^9 and compares reciprocals by linear arithmetic.
Claim. With $\varphi = (1+\sqrt{5})/2$, one has $\varphi^{-44} > 5.5 \times 10^{-10}$.
background
This module certifies the Recognition Science interval prediction for the baryon-to-photon ratio: $\varphi^{-44} \in (5.5\times 10^{-10},, 7.5\times 10^{-10})$. The observed Planck 2018 value $\eta_B = (6.10\pm 0.04)\times 10^{-10}$ sits inside that band.
The exponent 44 is structural: $44 = 4\times 11 = (\mathrm{flip_count\ on\ axis\ 0})\times(\mathrm{torsion\ gap},\Delta\tau_{12})$, the same integer that appears in the RS formula for $\alpha^{-1}$. Bounds on $\varphi^{\pm 44}$ are obtained from the Fibonacci closed form $\varphi^{44} = F_{44}\varphi + F_{43}$ together with the crude enclosure $\varphi\in(1.61,1.62)$.
The immediate upstream fact is $\varphi^{44} < 1.6\times 10^9$ (proved via the Fibonacci identity and $\varphi < 1.62$). A conversion lemma equates the real and natural powers $\varphi^{44}$.
proof idea
Rewrite $\varphi^{-44}$ as $(\varphi^{44})^{-1}$ via Real.rpow_neg and the conversion lemma that identifies real and natural powers of $\varphi$ at 44. Invoke the upstream upper bound $\varphi^{44} < 1.6\times 10^9$ and positivity of $\varphi^{44}$. Reciprocals reverse the inequality, so $(\varphi^{44})^{-1} > (1.6\times 10^9)^{-1}$. A norm_num check gives $(1.6\times 10^9)^{-1}\ge 5.5\times 10^{-10}$, and linarith closes the chain.
why it matters
This is one of the two edge inequalities that assemble into eta_B_interval: $\varphi^{-44}\in(5.5,7.5)\times 10^{-10}$. That conjunction, together with the matching upper bound, the observed-value check, and the structural identity $44=\mathrm{flip_count}(0)\times|\Delta\tau_{12}|$, is packaged as the master certificate etaBCert.
In the broader RS picture the same integer 44 governs both $\alpha^{-1}$ and $\eta_B$, so the lower edge is not an ad-hoc numerical cut: it is the reciprocal of a Fibonacci-powered bound forced by $\varphi$. The module's target is the closed interval certificate that places the Planck $\eta_B$ measurement inside the RS prediction without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.