phi_pow_17_approx
plain-language theorem explainer
Coarse certified bounds place the golden-ratio power φ^17 strictly between 3500 and 3600 (true value ≈ 3571). Mass-comparison and lepton-ratio audits cite it to fix the sign of the raw τ/e discrepancy without needing a tight decimal expansion. The proof multiplies interval bounds on φ^8 and on φ, using positivity and pow_add.
Claim. With $\varphi$ the golden ratio, $3500 < \varphi^{17} < 3600$.
background
The module MassComparison is quarantined from the certified RS surface: it imports PDG 2024 experimental masses and compares them to φ-ladder predictions of the form $m = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$.
Here $\varphi$ is the self-similar fixed point forced at T6 (also Mathlib's Real.goldenRatio). Upstream interval lemmas supply $46.97 < \varphi^8 < 46.99$ and $1.618 < \varphi < 1.6185$, together with $\varphi>0$. Those coarse brackets are enough to control $\varphi^{17}$ for sign-of-discrepancy arguments, not for high-precision metrology.
In the RS mass ladder the τ/e rung gap is 17, so $\varphi^{17}$ is the raw predicted mass ratio before radiative corrections.
proof idea
Tactic proof by interval arithmetic on powers. Import $\varphi^8\in(46.97,46.99)$ and $\varphi\in(1.618,1.6185)$ via the Numerics PhiBounds lemmas (rewritten under Constants.phi). Rewrite $\varphi^{16}=(\varphi^8)^2$ and $\varphi^{17}=\varphi^{16}\cdot\varphi$ by pow_add.
Lower bound: square the lower $\varphi^8$ bound with two mul_lt_mul_of_pos_* steps and positivity of $\varphi^8$, then multiply on the right by $1.618$; norm_num shows $3500 < 46.97^2\cdot 1.618$, and lt_trans closes.
Upper bound: symmetric argument with $46.99$ and $1.6185$, again chaining strict multiplications by positive factors, then norm_num for $46.99^2\cdot 1.6185 < 3600$.
why it matters
Feeds the KEY RESULT raw_prediction_discrepancy in the same module, which records that RS raw predictions sit on opposite sides of experiment for the two heavy leptons: $\varphi^{11}\approx 199$ under-shoots $m_\mu/m_e\approx 206.77$, while $\varphi^{17}\approx 3571$ over-shoots $m_\tau/m_e\approx 3477$ (both at the few-percent level). The doc-comment states these coarse bounds suffice to certify the sign of the raw τ/e discrepancy.
In the broader framework this is a verification lemma on the φ-ladder mass formula (yardstick × φ^{rung}), not a forcing-chain step. The parent theorem notes the framework claims radiative corrections close the gap; this bound only locks the uncorrected inequality direction. It sits downstream of T6 (φ forced) and the eight-tick / rung bookkeeping, and upstream of any certified comparison table against PDG 2024.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.