phi_pow_8_lower
plain-language theorem explainer
φ^8 exceeds 46.81. Researchers bounding the baryon asymmetry prefactor c_RS in Recognition Science cite this inequality to fix the lower edge of the washout interval. The proof rewrites the power via the Fibonacci closed form and feeds the known lower bound on φ into a linear arithmetic solver.
Claim. $φ^8 > 46.81$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module derives numerical bounds on powers of the golden ratio to obtain the interval for the prefactor c_RS = (1 − φ^{−8})^2 that appears in the baryogenesis formula η_B = c_RS × (algebraic content from the integration-gap rung). The upstream Fibonacci identity states that φ^8 = 21φ + 13, obtained stepwise from the defining relation φ^2 = φ + 1. A companion lemma supplies the tighter lower bound φ > 1.61.
proof idea
The term proof rewrites the left-hand side with the Fibonacci identity theorem, asserts φ > 1.61 from the upstream lemma, and concludes the inequality by linarith.
why it matters
The bound is invoked directly by the companion theorem that establishes φ^{−8} < 0.02137, which together fix the numerical band for c_RS and the predicted η_B interval (6.0 to 6.2)×10^{−10} containing the Planck value. It supplies one concrete numerical step inside the eight-tick washout construction of the T7 octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.