phi_pow4
plain-language theorem explainer
The lemma establishes the algebraic relation φ⁴ = 3φ + 2 for the golden ratio. Neutrino mass hierarchy calculations cite this identity when scaling estimates by successive powers of φ to match observed squared-mass differences. The short tactic proof derives the relation by successive multiplication from the base identity φ² = φ + 1 followed by ring normalization at each step.
Claim. $φ^4 = 3φ + 2$, where $φ = (1 + √5)/2$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module addresses observed mass differences Δm²₂₁ and Δm²₃₁ for neutrinos. The golden ratio φ is introduced via its defining quadratic equation, with the upstream lemma phi_sq_eq supplying the identity φ² = φ + 1 that generates all higher powers on the phi-ladder. This ladder supplies the scaling yardsticks for mass formulas in the Recognition framework.
proof idea
The tactic proof first obtains φ² = φ + 1 from phi_sq_eq. It then computes φ³ = 2φ + 1 by rewriting the successor power and applying ring_nf twice. The target φ⁴ = 3φ + 2 follows by one further successor step and ring normalization, after which exact closes the goal.
why it matters
The identity feeds directly into the downstream theorem mass_ratio_phi4, which bounds the ratio of neutrino mass estimates to within 0.2 of φ⁴. It supplies a concrete rung on the phi-ladder lattice required for the mass hierarchy predictions, consistent with the self-similar fixed point (T6) and the eight-tick octave structure of the forcing chain. The step closes an algebraic prerequisite for linking the Recognition Composition Law to observable neutrino data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.