phi51_lt
plain-language theorem explainer
The lemma establishes that the golden ratio to the 51st power is strictly less than 45537549354. It is invoked inside the electroweak masses module to close the numerical interval for the predicted Z boson mass. The proof is a one-line wrapper that rewrites the Recognition Science constant phi to the golden ratio and applies a pre-established numerical bound.
Claim. Let $phi$ denote the golden ratio. Then $phi^{51} < 45537549354$.
background
The ElectroweakMasses module places the Z boson at rung 1 on the phi-ladder, giving the mass formula m_Z = 2 * phi^51 / 10^6 MeV. The local constant phi is identified with the golden ratio by the sibling lemma phi_eq_goldenRatio, which unfolds Constants.phi and Real.goldenRatio and applies ring. This numerical bound is a prerequisite for the tight interval claimed in the downstream Z mass theorem.
proof idea
The term-mode proof rewrites Constants.phi via phi_eq_goldenRatio and then applies the theorem phi_pow51_lt from Numerics.Interval.PhiBounds exactly.
why it matters
The lemma supplies the final numerical step for z_mass_bounds, which asserts the Z prediction lies inside (91075.09, 91075.10) MeV. It implements the mass formula yardstick * phi^(rung-8+gap(Z)) at rung 1 for the electroweak sector and connects to the eight-tick octave and phi fixed-point structure of the forcing chain. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.