phi_tenth_eq
The lemma establishes the identity φ¹⁰ = 55φ + 34, extending the Fibonacci recurrence pattern for powers of the golden ratio. Researchers deriving RS constants or phi-ladder mass formulas would cite this step when scaling the recurrence upward. The proof is a direct calc chain that multiplies the ninth-power identity by φ, distributes, substitutes the quadratic φ² = φ + 1, and simplifies by ring.
claim$φ^{10} = 55φ + 34$
background
The golden ratio φ is defined to satisfy the quadratic equation whose positive root yields φ² = φ + 1. The Constants module constructs a chain of identities φ^n = F_n φ + F_{n-1} (F_n the Fibonacci sequence) that arise from repeated application of this quadratic. The local setting is the RS-native time quantum τ₀ = 1 tick, with φ emerging as the self-similar fixed point in the forcing chain. Upstream, phi_ninth_eq supplies φ⁹ = 34φ + 21 and phi_sq_eq supplies the base relation φ² = φ + 1.
proof idea
The proof is a calc block. It rewrites φ¹⁰ as φ · φ⁹, substitutes the ninth-power identity to obtain φ · (34φ + 21), distributes to 34φ² + 21φ, replaces φ² by φ + 1 via phi_sq_eq, and finishes with ring to reach 55φ + 34.
why it matters in Recognition Science
This lemma is invoked directly by phi_eleventh_eq to obtain the next recurrence step φ¹¹ = 89φ + 55. The sequence of such identities populates the phi-ladder used for mass formulas and RS-native constants (G = φ⁵/π, ħ = φ^{-5}). It instantiates the self-similar fixed-point property of φ forced at T6 of the UnifiedForcingChain.
scope and limits
- Does not prove the general Binet-style closed form for arbitrary φ^n.
- Does not derive φ itself from the J-cost functional equation.
- Does not map the identity onto specific physical constants such as α or G.
Lean usage
calc phi^11 = phi * phi^10 := by ring _ = phi * (55 * phi + 34) := by rw [phi_tenth_eq]formal statement (Lean)
201lemma phi_tenth_eq : phi^10 = 55 * phi + 34 := by
proof body
Tactic-mode proof.
202 calc phi^10 = phi * phi^9 := by ring
203 _ = phi * (34 * phi + 21) := by rw [phi_ninth_eq]
204 _ = 34 * phi^2 + 21 * phi := by ring
205 _ = 34 * (phi + 1) + 21 * phi := by rw [phi_sq_eq]
206 _ = 55 * phi + 34 := by ring
207
208/-- Key identity: φ¹¹ = 89φ + 55 (Fibonacci recurrence). -/