phi_rpow_44
plain-language theorem explainer
Equates the real power φ^44 with the natural-number power φ^44. Downstream interval bounds on φ^(-44) rewrite through this bridge before inverting the Fibonacci-based estimates of φ^44. The proof is a one-line application of the Mathlib cast identity for real powers of naturals.
Claim. For the golden ratio $\varphi$, the real exponentiation $\varphi^{44}$ (with exponent in $\mathbb{R}$) equals the ordinary natural power $\varphi^{44}$ (with exponent in $\mathbb{N}$).
background
The module certifies the Recognition Science interval for the baryon-to-photon ratio: $\varphi^{-44}\in(5.5\times10^{-10},7.5\times10^{-10})$, which contains the Planck 2018 value $\eta_B\approx6.1\times10^{-10}$. The integer 44 is structural: $44=4\times11$, the product of the axis-0 flip count and the torsion gap $\Delta\tau_{12}$, the same 44 that appears in the RS formula for $\alpha^{-1}$.
Powers of $\varphi$ are controlled via the Fibonacci closed form $\varphi^n=F_n\varphi+F_{n-1}$. Sibling lemmas bound the natural power $\varphi^{44}$ between $1.5\times10^9$ and $1.6\times10^9$. Negative real exponents are then obtained by inversion, which requires aligning the real-power notation used in $\varphi^{-44}$ with those natural-power bounds.
proof idea
One-line term proof: apply Mathlib's Real.rpow_natCast at base $\varphi$ and exponent 44. That lemma states that for any real $x$ and natural $n$, the real power $x^n$ coincides with the iterated product power, so the two Lean notations become definitionally interchangeable after the rewrite.
why it matters
Parent theorems phi_pow_neg44_lower and phi_pow_neg44_upper both open by rewriting Real.rpow_neg and then this lemma, converting $\varphi^{-(44:\mathbb{R})}$ into the reciprocal of the natural power already bounded by phi_pow_44_lower and phi_pow_44_upper. Those four inequalities assemble into eta_B_interval, the module's main certificate that $\varphi^{-44}$ lies in the observational window for $\eta_B$.
In the broader RS picture the same integer 44 links baryon asymmetry to the electromagnetic coupling (the $\alpha^{-1}$ formula with $44\pi$), so a clean real/nat power bridge is bookkeeping that keeps the interval certificate fully formal. No open scaffold remains here; the lemma is closed Mathlib glue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.