phi_pow_44_fib
plain-language theorem explainer
The equality phi to the 44th power equals 701408733 times phi plus 433494437 is established. Cosmologists bounding the baryogenesis parameter eta_B cite this exact coefficient to derive the numerical interval for phi to the minus 44. The proof is a direct instantiation of the general phi power Fibonacci identity at exponent 43 followed by substitution of the known Fibonacci numbers via native computation.
Claim. $phi^{44} = 701408733 phi + 433494437$ where $phi$ is the golden ratio.
background
In the eta_B prefactor derivation the module computes high negative powers of the golden ratio using its Fibonacci representation to bound the washout factor. The upstream theorem phi_pow_fib states that phi to the power n plus one equals the n plus one Fibonacci number times phi plus the nth Fibonacci number. This supplies the concrete coefficients needed for the subsequent bounds on phi to the minus 44 that enter the predicted eta_B interval.
proof idea
The proof instantiates the upstream phi_pow_fib theorem at argument 43 to obtain phi to the 44 equals fib 44 times phi plus fib 43. It then applies native_decide to confirm the concrete values Nat.fib 44 equals 701408733 and Nat.fib 43 equals 433494437. These values are substituted by simp and the goal is closed by exact.
why it matters
This result is invoked directly by the bounding lemmas phi_zpow_neg44_lower and phi_zpow_neg44_upper in the same module. Those lemmas combine the exact coefficients with the interval phi in (1.61, 1.62) to place c_RS times phi to the minus 44 inside (6.0 times 10 to the minus 10, 6.2 times 10 to the minus 10), matching the Planck eta_B measurement. It completes the explicit Fibonacci step in the chain from the general identity to the predicted baryon asymmetry band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.