phi17_lt
plain-language theorem explainer
The lemma proves that the golden ratio to the 17th power is strictly less than 3574. Workers checking lepton mass predictions against PDG data cite it when bounding the tau-to-electron ratio error. The tactic proof rewrites phi to the golden ratio, invokes pre-established bounds on phi^8 and phi, decomposes the exponent by ring normalization, multiplies the inequalities, and closes with linear arithmetic.
Claim. $phi^{17} < 3574$ where $phi$ is the golden ratio satisfying $phi = (1 + sqrt(5))/2$.
background
The Masses.Verification module compares RS lepton mass predictions to PDG 2024 values. The formula used is m(Lepton, r) = phi^{57+r} / (2^{22} * 10^6) in MeV for B_pow = -22 and r0 = 62. Upstream results include phi_eq_goldenRatio equating Constants.phi to Real.goldenRatio, phi_lt_16185 giving phi < 1.6185, and phi_pow8_lt supplying the bound on phi^8.
proof idea
Rewrite via phi_eq_goldenRatio. Obtain h8_hi from phi_pow8_lt and hφ_hi from phi_lt_16185. Establish positivity of the terms. Decompose the 17th power as phi^8 * phi^8 * phi by ring_nf. Apply mul_lt_mul twice to reach the product bound 46.99^2 * 1.6185. Finish with linarith showing the product is less than 3574.
why it matters
The bound is invoked inside tau_electron_ratio_error to establish that the relative error between the predicted and experimental tau-to-electron ratio stays below 0.03. It supplies a concrete numerical check for the phi-ladder rung at exponent 17 in the lepton sector. The result aligns with the self-similar fixed point and eight-tick octave from the forcing chain while remaining quarantined from the certified derivation of the mass formula itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.