phi_eleventh_eq
The golden ratio satisfies φ¹¹ = 89φ + 55 via the Fibonacci recurrence. Researchers deriving mass hierarchies on the phi-ladder cite this identity to bound ratios at rung 11. The proof is a short calc chain that multiplies the tenth-power identity by φ and reduces the resulting quadratic term with the base relation φ² = φ + 1.
claimLet φ be the positive root of x² - x - 1 = 0. Then φ¹¹ = 89φ + 55.
background
The Constants module builds canonical RS quantities from the golden ratio φ. The defining relation φ² = φ + 1 is recorded in phi_sq_eq, quoted as 'Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0)'. The preceding step phi_tenth_eq supplies φ¹⁰ = 55φ + 34, obtained by the same recurrence pattern. These identities sit inside the broader phi-ladder construction used for mass formulas of the form yardstick · φ^(rung - 8 + gap(Z)).
proof idea
The tactic proof opens a calc block with φ¹¹ = φ · φ¹⁰. It rewrites the tenth power via phi_tenth_eq, distributes with ring, substitutes φ² = φ + 1 from phi_sq_eq, and collects coefficients with a final ring step to reach 89φ + 55.
why it matters in Recognition Science
This lemma is invoked directly by phi_11_hierarchy_lower to prove φ¹¹ > 180, supplying the explicit Fibonacci coefficients needed for conservative hierarchy bounds. It fills the rung-11 slot in the phi-ladder that supports the mass formula and aligns with the self-similar fixed point at T6. The downstream doc-comment notes the hierarchy structure: 'Mass ratios are φ-powers of integer differences.'
scope and limits
- Does not prove irrationality or other algebraic properties of φ.
- Does not supply numerical approximations or error bounds.
- Does not extend the identity to negative exponents or composite bases.
- Does not embed physical units or couple to constants such as G or α.
Lean usage
rw [phi_eleventh_eq]formal statement (Lean)
209lemma phi_eleventh_eq : phi^11 = 89 * phi + 55 := by
proof body
Tactic-mode proof.
210 calc phi^11 = phi * phi^10 := by ring
211 _ = phi * (55 * phi + 34) := by rw [phi_tenth_eq]
212 _ = 55 * phi^2 + 34 * phi := by ring
213 _ = 55 * (phi + 1) + 34 * phi := by rw [phi_sq_eq]
214 _ = 89 * phi + 55 := by ring
215
216/-! ### Canonical constants derived from φ -/
217
218/-- Canonical locked fine-structure constant: α_lock = (1 − 1/φ)/2. -/