phi_pow_44_gt_1pt5e9
plain-language theorem explainer
A numerical inequality establishes that the golden ratio to the 44th power exceeds 1.5 billion. Cosmologists deriving the baryon asymmetry from Recognition Science's phi-ladder would cite this result to anchor the predicted eta value. The proof reduces the expression via the Fibonacci recurrence relation for powers of phi and applies a lower bound on phi together with linear arithmetic to confirm the inequality.
Claim. $phi^{44} > 1.5 times 10^{9}$
background
The module COS-007 derives the matter abundance eta ~ 10^{-10} from phi-structure in Recognition Science, attributing the small excess of matter over antimatter to CP violation in the 8-tick phase structure. Key definitions include the golden ratio phi as the self-similar fixed point and the Fibonacci sequence appearing in the closed-form expression for its powers. This lemma depends on the identity phi^{n+1} = F_{n+1} phi + F_n from phi_pow_fib_succ and the bound phi > 1.61 from the Constants module.
proof idea
The tactic proof first rewrites the real exponentiation as a natural number power. It invokes phi_pow_fib_succ at 43 to obtain the exact linear combination with Fibonacci coefficients 701408733 and 433494437, which are inserted via native_decide. The lower bound phi > 1.61 is multiplied through and the resulting inequality is discharged by linarith.
why it matters
It supplies the lower bound needed for the parent theorem phi_power_matches_eta, which verifies that phi to the minus 44 lies close to the observed baryon-to-photon ratio eta_B = 6.1e-10. This anchors the RS prediction for baryogenesis arising from the eight-tick octave (T7) and the specific 44 = 4 x 11 structure. The module points to a PRD paper on baryogenesis from Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.