phi59_gt
plain-language theorem explainer
The lemma asserts that 2138898000000 is strictly less than the golden ratio raised to the 59th power. Researchers verifying lepton mass predictions on the phi-ladder against PDG data would cite this numerical anchor. The proof is a one-line wrapper that rewrites the Recognition Science constant phi to the golden ratio and invokes the pre-proved bound from the PhiBounds module.
Claim. $2138898000000 < phi^{59}$ where $phi$ is the golden ratio as defined in the Constants module.
background
The Masses.Verification module compares integer-rung mass predictions to PDG 2024 experimental values, treating the latter as imported constants. For leptons the formula is $m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6)$ in MeV. The constant phi is identified with the golden ratio by the sibling lemma phi_eq_goldenRatio, which states Constants.phi = Real.goldenRatio.
proof idea
The proof is a one-line wrapper. It rewrites Constants.phi via phi_eq_goldenRatio to obtain the golden ratio, then applies the exact numerical theorem phi_pow59_gt from Numerics.Interval.PhiBounds.
why it matters
This bound is used by the downstream theorem electron_mass_bounds to place the predicted electron mass inside the interval (0.5098, 0.5102) MeV. It supplies a concrete numerical step in the lepton-sector verification of the phi-ladder mass formula (B_pow = -22, r0 = 62) inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.