phi_eq_goldenRatio
plain-language theorem explainer
The lemma identifies the Recognition Science constant phi with the classical golden ratio. Downstream electroweak bounds and Weinberg-angle lemmas cite it to import known inequalities on powers of phi; the astrophysics IMF theorem also reuses the identification. The proof is a direct term-mode unfolding followed by ring normalization.
Claim. $phi = (1 + sqrt(5))/2$
background
The ElectroweakMasses module predicts boson masses on the phi-ladder: m_Z equals 2 * phi^51 / 10^6 MeV, m_W follows from m_Z * cos theta_W, and sin^2 theta_W equals (3 - phi)/6. Constants.phi is the self-similar fixed point imported from the CPM bundle. Upstream equality lemmas in ObservabilityLimits and Verification perform the same identification so that golden-ratio inequalities can be applied uniformly across mass and astrophysics calculations.
proof idea
One-line term proof. It unfolds Constants.phi and Real.goldenRatio then invokes ring to confirm the algebraic identity.
why it matters
The equality supplies the numerical bounds phi51_gt and phi51_lt that locate m_Z inside (91075.09, 91075.10) MeV and enables the positivity proof for sin2_theta_W_rs. It also feeds the IMF slope result showing alpha close to phi^2. In the framework it completes the T6 identification of the forced fixed point with the classical golden ratio, closing the zero-parameter route from the forcing chain to electroweak observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.