phi_seventh_eq
φ^7 equals 13φ + 8 for the golden ratio φ. Workers deriving Recognition Science constants cite this Fibonacci recurrence when extending the phi-ladder for mass and coupling formulas. The proof is a short calc chain that multiplies the sixth-power identity by φ, expands, substitutes the square relation φ² = φ + 1, and simplifies.
claim$φ^7 = 13φ + 8$
background
The golden ratio φ satisfies the quadratic equation φ² = φ + 1 by definition and generates the sequence of power identities φ^n = F_n φ + F_{n-1} where F_n are Fibonacci numbers. This lemma continues that sequence at n = 7. The module Constants builds these identities from the quadratic relation onward in RS-native units where the fundamental time quantum is one tick.
proof idea
A calc block begins with φ^7 = φ · φ^6 by ring, rewrites the right-hand side using phi_sixth_eq to obtain φ · (8φ + 5), expands by ring, replaces φ² with φ + 1 via phi_sq_eq, and finishes with ring to reach 13φ + 8.
why it matters in Recognition Science
The lemma is invoked directly by the eighth-power identity φ^8 = 21φ + 13, extending the Fibonacci chain that supports the eight-tick octave (T7) and the phi-ladder mass formula. It contributes to the derivation of RS-native constants such as G = φ^5 / π and the alpha band inside (137.030, 137.039).
scope and limits
- Does not derive the numerical value or irrationality of φ.
- Does not prove the general Fibonacci recurrence for arbitrary powers.
- Does not connect the identity to J-cost or forcing-chain steps T0–T8.
- Does not address physical units or measurement predictions.
Lean usage
calc phi^8 = phi * phi^7 := by ring _ = phi * (13 * phi + 8) := by rw [phi_seventh_eq] _ = 13 * phi^2 + 8 * phi := by ring _ = 13 * (phi + 1) + 8 * phi := by rw [phi_sq_eq] _ = 21 * phi + 13 := by ringformal statement (Lean)
177lemma phi_seventh_eq : phi^7 = 13 * phi + 8 := by
proof body
Tactic-mode proof.
178 calc phi^7 = phi * phi^6 := by ring
179 _ = phi * (8 * phi + 5) := by rw [phi_sixth_eq]
180 _ = 8 * phi^2 + 5 * phi := by ring
181 _ = 8 * (phi + 1) + 5 * phi := by rw [phi_sq_eq]
182 _ = 13 * phi + 8 := by ring
183
184/-- Key identity: φ⁸ = 21φ + 13 (Fibonacci recurrence). -/