phi_pow_44_fib
plain-language theorem explainer
Exact closed form φ^44 = 701408733 φ + 433494437 via the Fibonacci–φ identity. Cosmology proofs that bound φ^44 (and hence η_B ∼ φ^{-44}) cite this equality before applying φ ∈ (1.61, 1.62). Proof instantiates the inductive identity at n = 43 and discharges the two Fibonacci values by native_decide.
Claim. Let $\varphi$ be the golden ratio. Then $\varphi^{44} = F_{44}\,\varphi + F_{43}$, where $F_{44} = 701408733$ and $F_{43} = 433494437$ are the ordinary Fibonacci numbers (with $F_0 = 0$, $F_1 = 1$).
background
The module certifies the RS interval prediction $\varphi^{-44}\in(5.5\times 10^{-10},7.5\times 10^{-10})$ for the baryon-to-photon ratio $\eta_B$. The observed Planck 2018 value sits inside that band. The integer 44 is structural: $44=4\times 11=(\text{flip count on axis }0)\times(\text{torsion gap }\Delta\tau_{12})$, the same 44 that appears in the $\alpha^{-1}$ formula.
Powers of $\varphi$ obey the classical Fibonacci identity $\varphi^{n+1}=F_{n+1}\varphi+F_n$. The private lemma phi_pow_fib proves this by induction on $n$ for the RS constant $\varphi$. Specializing at exponent 44 converts an abstract power into an explicit linear form in $\varphi$, which is then easy to bound once $\varphi\in(1.61,1.62)$ is known.
Two Fibonacci conventions appear in the repo (Mathlib-style $F_0=0,F_1=1$ versus a shifted $1,1,2,\ldots$ sequence). The identity used here is the standard Mathlib indexing.
proof idea
One specialization of the inductive identity. Apply phi_pow_fib at $n=43$ to obtain $\varphi^{44}=F_{44}\varphi+F_{43}$. Discharge $F_{44}=701408733$ and $F_{43}=433494437$ by native_decide, rewrite those numerals into the identity, and close by exact.
why it matters
This is the algebraic hinge of the $\varphi^{44}$ interval certificate. Downstream, phi_pow_44_lower and phi_pow_44_upper rewrite through this equality and finish with nlinarith under $\varphi>1.61$ and $\varphi<1.62$, yielding $1.5\times 10^9<\varphi^{44}<1.6\times 10^9$. The prefactor module reuses the same rewrite for tighter bounds on $\varphi^{-44}$ ($\approx 6.37$–$6.40\times 10^{-10}$), which feed eta_B_interval and the master EtaBCert.
In the broader RS picture the exponent 44 is not free: it is the product of chirality flip count and the torsion gap, linking baryon asymmetry to the same structural integer that governs $\alpha^{-1}$. The lemma itself is pure number theory; its place in the framework is to make that shared integer numerically controllable on the $\varphi$-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.