phi_pow51_eq
plain-language theorem explainer
The equality equates φ^51 exactly to the linear combination 20365011074 φ + 12586269025, where the coefficients are the 51st and 50th Fibonacci numbers. Analysts deriving rigorous numerical bounds on powers of the golden ratio for Recognition Science constant verification would cite this identity. The proof invokes the closed-form relation goldenRatio * fib(51) + fib(50) = goldenRatio^51, substitutes the explicit integer values via norm_num, and rearranges with commutativity and associativity.
Claim. $φ^{51} = 20365011074 · φ + 12586269025$
background
The module Numerics.Interval.PhiBounds supplies rigorous algebraic bounds on φ = (1 + √5)/2. It relies on the Fibonacci sequence, defined recursively in upstream modules as fib 0 = 1, fib 1 = 1 and fib (n+2) = fib n + fib (n+1), together with the defining relation φ² = φ + 1 that extends to higher powers. Upstream results include add_assoc and add_comm from Foundation.ArithmeticFromLogic establishing associativity and commutativity of addition, plus multiple fib definitions from Gap45.Derivation and RamanujanBridge modules that supply the sequence values.
proof idea
The proof applies the lemma Real.goldenRatio_mul_fib_succ_add_fib 50 to obtain goldenRatio * (Nat.fib 51) + Nat.fib 50 = goldenRatio^51. It replaces the Fibonacci numbers with their explicit integer values 20365011074 and 12586269025 via norm_num. It then finishes with simpa using mul_comm, mul_left_comm, add_comm, add_left_comm and add_assoc to reach the target form.
why it matters
This supplies the exact algebraic identity required by the downstream theorems phi_pow51_gt and phi_pow51_lt that bound φ^51 between 45537548334 and 45537549354. It supports numerical verification steps in the Recognition framework for the phi-ladder mass formulas and the α^{-1} interval (137.030, 137.039), using the self-similar fixed-point property of φ. The result closes a concrete computation needed for the eight-tick octave and D = 3 derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.