phi10_fibonacci
plain-language theorem explainer
The golden ratio satisfies φ^10 = 55φ + 34, matching the Fibonacci combination F(11)φ + F(10). Physicists deriving the weak force in Recognition Science cite this to express the Fermi constant G_F = φ^{-10}/(8 m_W²) in native units. The proof invokes the base relation φ² = φ + 1, builds the first five powers by linear arithmetic, squares the fifth power, and reduces the result algebraically.
Claim. $φ^{10} = 55φ + 34$
background
The module derives the weak nuclear force from Recognition Science by setting G_F = φ^{-10}/(8 m_W²) in RS-native units, with φ^10 expanded via the Fibonacci relation. The golden ratio φ is defined by the quadratic x² - x - 1 = 0, so the upstream lemma phi_sq_eq states φ² = φ + 1. This supplies the explicit coefficient needed to evaluate φ^{-10} without further hypotheses.
proof idea
The tactic proof first obtains phi_sq_eq. It derives the next three powers (φ³ = 2φ + 1, φ⁴ = 3φ + 2, φ⁵ = 5φ + 3) by nlinarith. It rewrites φ^{10} as (φ⁵)² by ring, then applies nlinarith to the resulting linear combination.
why it matters
The identity is used directly by phi10_gt_100 and by the weakForceCert definition that packages the five decay types, the φ^{10} value, and the bound >100. It realizes the Fibonacci structure on the phi-ladder that appears in the mass formula and the eight-tick octave. The result closes the algebraic step required to write G_F in terms of φ inside the weak-force certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.