phi_pow7
plain-language theorem explainer
The lemma establishes that the seventh power of the golden ratio satisfies φ⁷ = 13φ + 8. Researchers modeling neutrino mass ratios in Recognition Science would cite this when scaling the phi-ladder to the seventh rung. The proof proceeds by successive application of the recurrence φ^{n+1} = φ · φ^n starting from the base identity φ² = φ + 1, with ring normalization at each step.
Claim. Let φ be the golden ratio satisfying φ² = φ + 1. Then φ⁷ = 13φ + 8.
background
In the StandardModel.NeutrinoMassHierarchy module the focus is on observed mass differences expressed through powers of the golden ratio. The golden ratio φ = (1 + √5)/2 obeys the minimal polynomial x² - x - 1 = 0, which yields the key recurrence φ² = φ + 1. This recurrence is supplied by the upstream lemma phi_sq_eq (both in Constants and in PhiLadderLattice), which is invoked verbatim at the start of the proof.
proof idea
The tactic proof first obtains φ² = φ + 1 from phi_sq_eq. It then builds the next five powers one by one: each step applies pow_succ to the previous result, rewrites with the base identity, and normalizes with ring_nf. The final step yields exactly φ⁷ = 13φ + 8, which is returned by exact.
why it matters
The result is used directly by the downstream theorem mass_ratio_phi7, which bounds the observed neutrino mass ratio against a multiple of φ⁷. It supplies the precise coefficient needed for the seventh rung of the phi-ladder in the Recognition Science mass formula, consistent with the self-similar fixed point (T6) and the eight-tick octave structure. No scaffolding remains; the identity is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.