phi_pow_8_fib
plain-language theorem explainer
Golden ratio powers satisfy the Fibonacci recurrence, yielding φ^8 = 21φ + 13. Researchers deriving the baryon-to-photon ratio η_B in Recognition Science cite this algebraic identity to bound the prefactor c_RS. The tactic proof reduces the eighth power by successive squaring from the base equation φ^2 = φ + 1, applying ring normalization and linear arithmetic at each step.
Claim. $φ^8 = 21φ + 13$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module derives the prefactor in the baryogenesis formula η_B = c × (algebraic content from integration-gap rung), with c_RS defined as (1 − φ^{−8})^2. This squared form represents independent washout channels for matter and antimatter sectors, each at rate φ^{−8} corresponding to one rung per fundamental tick at D = 3. The present theorem supplies the exact algebraic value of φ^8 needed for subsequent numerical bounds.
proof idea
The proof begins by importing the base relation φ^2 = φ + 1 via phi_sq_eq. It derives φ^4 = 3φ + 2 through expansion and reduction with ring_nf followed by linarith. It then sets φ^8 = φ^4 * φ^4, substitutes the expression for φ^4, and reduces again with ring_nf and linarith to reach 21φ + 13.
why it matters
This result is used directly by the bounding theorems phi_pow_8_lower and phi_pow_8_upper in the same module. Those bounds feed the calculation of c_RS · φ^{−44} in the interval (6.0 × 10^{-10}, 6.2 × 10^{-10}), matching the Planck 2018 value of η_B. It realizes the eight-tick octave step in the forcing chain, where φ^{-8} quantifies the washout per octave in three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.