phi51_gt
plain-language theorem explainer
The lemma asserts that 45537548334 is strictly less than the golden ratio to the 51st power. It is invoked when bounding the predicted Z boson mass in the electroweak sector of the Recognition framework. The proof is a one-line wrapper that substitutes the definition of phi and applies the numeric bound from the PhiBounds module.
Claim. $45537548334 < phi^{51}$ where $phi$ is the golden ratio.
background
The module derives electroweak boson masses from the phi-ladder. The Z boson is assigned rung 1, so its mass formula reads $m_Z = 2 times phi^{51} / 10^6$ in MeV. The constant phi is identified with the golden ratio via the equality Constants.phi = goldenRatio. Upstream results supply this identification in multiple modules and the strict numeric inequality $45537548334 < goldenRatio^{51}$ from the PhiBounds library.
proof idea
The proof is a one-line wrapper. It rewrites Constants.phi to goldenRatio using the local phi_eq_goldenRatio lemma, then applies the exact theorem phi_pow51_gt from Numerics.Interval.PhiBounds.
why it matters
The lemma supplies the numeric anchor for the downstream z_mass_bounds theorem, which confines the Z prediction to the interval (91075.09, 91075.10) MeV. It completes the concrete evaluation of the rung-1 mass formula in the electroweak sector, consistent with the phi self-similar fixed point and the eight-tick octave structure. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.