phi_pow_7_eq
plain-language theorem explainer
Algebraic identity φ^7 = 13φ + 8 is proved here and cited for the neutrino mass-squared ratio m₃²/m₂² = φ^7 in Recognition Science. It enables the interval bounds (28, 30) matching experiment near 29. Proof uses successive substitution from φ^6 = 8φ + 5 and φ² = φ + 1 via ring normalization.
Claim. $φ^7 = 13φ + 8$
background
The module proves rigorous bounds on Recognition Science mass predictions using powers of the golden ratio φ. Key quantities include φ^6 for baryon ratios and φ^7 for neutrino squared-mass ratios. The golden ratio satisfies φ² = φ + 1 by definition from the quadratic equation x² - x - 1 = 0. Upstream results supply the base identities: Key identity: φ⁶ = 8φ + 5 (Fibonacci recurrence). The defining identity of the golden ratio: φ² = φ + 1. These allow inductive computation of higher powers via the Fibonacci recurrence inherent to φ.
proof idea
The proof is a calc block that starts from φ^7 = φ · φ^6, substitutes the sixth-power identity to obtain φ(8φ + 5), expands by ring to 8φ² + 5φ, replaces φ² with φ + 1 to reach 8(φ + 1) + 5φ, and simplifies by ring to 13φ + 8. It invokes phi_sixth_eq and phi_sq_eq.
why it matters
This identity is used by the bounding theorems phi_pow_7_gt_28, phi_pow_7_gt_29 and phi_pow_7_lt_30 to place φ^7 in (28, 30), confirming the neutrino ratio prediction. It also supports the derivation of φ^11 = 89φ + 55 for quark ratios. Within the framework it supplies the sharpest seam-free prediction, relying on the phi-ladder structure from the NumberTheory module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.