phi_pow_8_upper
plain-language theorem explainer
The declaration proves that the eighth power of the golden ratio satisfies φ^8 < 47.03. Cosmologists deriving the baryon asymmetry prefactor η_B in Recognition Science would cite this to fix the upper edge of the washout interval. The proof is a term-mode wrapper that substitutes the Fibonacci closed form for φ^8 and applies the independent bound φ < 1.62 together with linear arithmetic.
Claim. $φ^8 < 47.03$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module derives the order-one prefactor c_RS = (1 − φ^{−8})^2 in the baryogenesis formula η_B = c × (integration-gap content). The squared form encodes independent washout of matter and antimatter sectors, each carrying one rung of fermionic degrees of freedom at rate φ^{−8} per fundamental tick in D = 3. The present theorem supplies the concrete upper bound on φ^8 required to obtain the matching lower bound on φ^{−8}.
proof idea
The proof is a term-mode wrapper. It rewrites the left-hand side via the Fibonacci identity theorem phi_pow_8_fib, reducing φ^8 to the linear expression 21φ + 13. It then introduces the hypothesis φ < 1.62 from the upstream lemma phi_lt_onePointSixTwo and closes immediately with linarith.
why it matters
This bound is invoked directly by the downstream theorem phi_zpow_neg8_lower to establish φ^{−8} > 0.02126. The pair of bounds pins φ^8 inside (46.81, 47.03) and thereby anchors the predicted interval (6.0 × 10^{−10}, 6.2 × 10^{−10}) for c_RS · φ^{−44}, which matches the Planck 2018 value of η_B. In the framework it instantiates the eight-tick octave (T7) at D = 3, providing the numerical anchor for the washout factor inside the Recognition Composition Law application to baryogenesis. The squared interpretive form of c_RS remains hypothesis-grade.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.