phi44_gt_1e8
plain-language theorem explainer
φ^44 exceeds 10^8. Cosmologists deriving baryon asymmetry from the Recognition Science phi-ladder cite this bound to place η_B below 10^{-8}. The proof reduces the exponent via ring identities on powers of φ then applies nlinarith to the product of the φ^32 and φ^12 lower bounds.
Claim. $φ^{44} > 10^{8}$ where $φ = (1 + √5)/2$ satisfies $φ^2 = φ + 1$.
background
The module develops the RS prediction η_B ≈ φ^{-44} for A3 Baryogenesis and supplies the supporting large-number bound φ^44 > 10^8. The phi-ladder generates successive integer powers of the golden ratio to produce the required scale separation between early-universe dynamics and observed asymmetry. Upstream results include the identity φ² = φ + 1 from Constants.phi_sq_eq and the tighter numerical bound φ > 1.61 from phi_gt_onePointSixOne; these feed the chain of explicit lower bounds on φ^8, φ^32 and now φ^44.
proof idea
The tactic proof first builds an auxiliary lower bound for φ^12 by expressing intermediate powers (φ^3 through φ^6) as linear forms in φ via repeated nlinarith from phi_sq_eq, then multiplies φ^6 by itself and invokes phi_gt_onePointSixOne. It rewrites φ^44 as φ^32 × φ^12, normalizes the constant, and finishes with nlinarith on the product of the known φ^32 > 4×10^6 bound and the new φ^12 bound.
why it matters
The theorem supplies the phi44_large field inside baryonAsymmetryCert and is invoked directly by etaB_small to obtain η_B < 10^{-8}. It completes the numerical requirement for the module's RS prediction η_B ≈ φ^{-44}. The result anchors the scale separation produced by the phi-ladder in the baryon-asymmetry calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.