phi_pow13
plain-language theorem explainer
The lemma shows that the golden ratio to the thirteenth power equals 233 times phi plus 144. Neutrino mass hierarchy work in Recognition Science cites it when linking phi-ladder relations to seesaw scales. The proof builds the identity iteratively from the base recurrence phi squared equals phi plus one via successive power expansions and ring normalization.
Claim. $phi^{13} = 233 phi + 144$, where $phi$ is the golden ratio satisfying $phi^2 = phi + 1$.
background
The module StandardModel.NeutrinoMassHierarchy addresses observed neutrino mass differences. It employs powers of the golden ratio phi in mass scale predictions. The key upstream identity phi squared equals phi plus one appears in Constants.phi_sq_eq, derived from the quadratic equation x squared minus x minus one equals zero, and is restated in NumberTheory.PhiLadderLattice.phi_sq_eq.
proof idea
The tactic proof introduces h2 as phi squared equals phi plus one from phi_sq_eq. It then applies pow_succ followed by ring_nf and substitution of the base identity repeatedly to obtain h3 through h13, each step advancing the exponent by one and updating the Fibonacci coefficients until reaching the target equality for the thirteenth power.
why it matters
This result feeds the theorem seesaw_scale_phi_connection, which bounds the phi-predicted Majorana scale near 2.3 times 10 to the 16 within an error of 10 to the 15. It supplies an explicit computational link in the phi-ladder for neutrino hierarchies, consistent with the self-similar fixed point phi from the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.