phi17_gt
plain-language theorem explainer
The lemma proves 3569 is strictly less than the golden ratio raised to the seventeenth power. Researchers checking lepton mass predictions against PDG data cite it when bounding the tau-to-electron ratio. The proof rewrites the power as a product of two eighth powers times phi, substitutes the lower bounds phi greater than 1.618 and phi to the eighth greater than 46.97, propagates them via multiplication inequalities, and closes with linear arithmetic.
Claim. $3569 < phi^{17}$ where $phi$ denotes the golden ratio.
background
The module compares predicted lepton masses to PDG 2024 values via the formula m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6) in MeV, with experimental inputs treated as imported constants. Phi is identified with the mathematical golden ratio by the equality theorem in the same module and in ElectroweakMasses. Upstream results supply the concrete bounds 1.618 less than phi and 46.97 less than phi to the eighth, which serve as the numerical anchors for this inequality.
proof idea
The tactic proof first applies the golden ratio identification, obtains the lower bounds for phi to the eighth and for phi, establishes positivity of the base terms, rewrites the seventeenth power as the product of two eighth powers times phi, applies the multiplication inequality twice to combine the bounds, and finishes with linarith to compare the resulting composite lower bound against 3569.
why it matters
This bound is invoked directly by the tau-electron ratio error theorem and the tau ratio overshoot theorem to keep the relative error below 0.03. It supplies a concrete numerical step in the lepton mass verification that uses the phi-ladder with rung offset tied to the eight-tick octave. The declaration closes a specific gap in the comparison of the predicted phi^17 term to experiment without addressing broader derivation of the mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.