one_minus_phi_neg8_lower
plain-language theorem explainer
This lemma establishes that 1 minus phi to the negative eighth exceeds 0.978. Cosmologists bounding the baryon asymmetry prefactor c_RS in the Recognition Science framework cite it to anchor the lower edge of the numerical interval. The proof is a one-line wrapper that imports the companion upper bound on phi to the negative eighth and applies linear arithmetic.
Claim. Let $phi$ denote the golden ratio. Then $1 - phi^{-8} > 0.978$.
background
The module derives the order-one prefactor c_RS in the baryogenesis formula eta_B = c_RS times algebraic content from the integration-gap rung. Here c_RS expands to (1 - phi^{-8})^2, with the exponent eight tracing to the eight-tick octave at D = 3. The upstream theorem phi_zpow_neg8_upper proves phi^{-8} < 0.02137 by inverting a Fibonacci-derived lower bound on phi^8.
proof idea
The proof is a one-line wrapper. It imports the upper bound phi^{-8} < 0.02137 from phi_zpow_neg8_upper and concludes the desired inequality by linear arithmetic.
why it matters
Four downstream theorems on the bounds and positivity of c_RS invoke this result. It supports the numerical prediction for eta_B that matches the Planck 2018 value within the stated band. The argument relies on the forced phi-ladder and the Recognition Composition Law for the self-similar structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.