phi_pow_residue_mu_upper_v2
plain-language theorem explainer
Physicists deriving upper limits on the muon mass within the Recognition Science lepton ladder cite this inequality to bound the golden-ratio-powered residue term below 0.00975. It supplies the numerical cap required for the predicted muon mass estimate. The tactic proof extracts a residue exponent strictly less than -9.625 from an interval lemma, rewrites phi as the golden ratio, and chains the strict monotonicity of the power function through transitivity to a pre-proven bound at exponent -9.625.
Claim. $phi^{r_μ} < 0.00975$, where $r_μ = (gap(1332) - refined_shift) + step_{eμ}$ is the predicted muon residue.
background
The Necessity module for lepton generations derives forced bounds on muon and tau masses from the electron structural mass and geometric constants. The predicted muon residue serves as the exponent in the mass formula and is defined as (gap 1332 minus refined shift) plus the electron-to-muon step function. This sits inside the T10 program that replaces lepton axioms with inequalities built from the eight-tick octave, cube geometry, and the phi-ladder.
proof idea
The proof invokes the residue bounds lemma to obtain predicted_residue_mu < -9.625. It rewrites phi as Real.goldenRatio, tightens the exponent inequality via linarith, then applies the strict monotonicity lemma for the golden ratio power together with lt_trans to transfer the bound from the prior theorem phi_pow_neg9625_upper_v2.
why it matters
This supplies the residue power bound used directly in predicted_mass_mu_upper_v2 to cap the predicted muon mass below 105.9. It advances the T10 necessity chain that forces lepton masses from the electron structural mass and constants such as E_passive, faces, W, and alpha. The result closes one link between the phi-ladder residue definitions and observable mass ratios without additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.