phi_eq_goldenRatio
plain-language theorem explainer
The lemma asserts that the Recognition Science constant phi coincides exactly with the classical golden ratio. Mass-prediction lemmas in ElectroweakMasses and ObservabilityLimits cite it to convert symbolic phi-powers into concrete numerical bounds for lepton and Z-boson masses. The proof is a one-line term that unfolds both definitions and applies the ring tactic.
Claim. The Recognition Science constant $phi$ equals the golden ratio $frac{1 + sqrt{5}}{2}$.
background
In Recognition Science the constant phi is the unique positive fixed point of the J-function, satisfying phi = 1 + 1/phi and arising at step T6 of the forcing chain. The module Masses.Verification compares integer-rung predictions of the form m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6) MeV against PDG 2024 data while treating experimental masses as imported constants. Upstream results in ElectroweakMasses and ObservabilityLimits already record the identical identification, enabling consistent evaluation of terms such as phi^{51}.
proof idea
The proof is a one-line term that unfolds Constants.phi and Real.goldenRatio then applies the ring tactic to obtain equality by direct algebraic simplification.
why it matters
Nineteen downstream declarations rely on this identification to bound phi-powers for mass predictions and to derive the IMF slope near phi^2 in imf_from_j_minimization. It supplies the concrete numerical bridge between the T6 self-similar fixed point and experimental checks in the phi-ladder mass formula. The same equality appears in sin2_theta_positive and the phi51_gt/lt bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.