phi_pow_residue_mu_upper
plain-language theorem explainer
Establishes that the golden ratio raised to the predicted muon residue lies strictly below 0.0098. Researchers closing the T10 lepton-ladder necessity argument cite it to obtain the muon-mass upper bound below 107. The tactic proof applies strict monotonicity of the power map to the residue interval and substitutes the pre-proved numeric fact at exponent -9.62.
Claim. $φ^{r_μ} < 0.0098$, where $φ$ is the golden ratio and $r_μ$ is the predicted muon residue defined by $(gap(1332) - refined_shift) + step_{eμ}$.
background
The T10 module shows the lepton ladder is forced once the electron structural mass and the geometric step functions are fixed. The predicted muon residue is the sum of the gap-1332 term minus refined shift plus the electron-to-muon step; its bounds lemma places the value inside (-9.63, -9.62). The upstream strict-monotonicity result states that $φ^x$ increases with $x$ for $φ > 1$, while the endpoint theorem supplies the concrete inequality $φ^{-9.62} < 0.0098$.
proof idea
The proof first obtains the residue upper bound from predicted_residue_mu_bounds. It rewrites $φ$ as goldenRatio and invokes phi_rpow_strictMono to replace the exponent -9.6265 by -9.62, yielding a strict inequality. The final step substitutes the already-proved numeric closure phi_pow_neg962_upper_proved.
why it matters
Supplies the upper half of phi_pow_residue_mu_bounds and is invoked inside predicted_mass_mu_upper and predicted_mass_mu_upper_tight to reach the concrete bound 106.4. It therefore closes the numeric seam required by the T10 claim that muon and tau masses follow from T9 electron mass plus the eight-tick and cube-derived constants without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.