predicted_residue_mu_bounds
plain-language theorem explainer
The lemma supplies numerical bounds on the predicted muon residue, defined as the gap term at 1332 minus the refined shift added to the electron-muon step. Researchers deriving lepton masses in the Recognition framework cite this to constrain the muon mass on the phi-ladder. The proof is a term-mode reduction that unfolds the definition and combines the pre-proven component intervals via linear arithmetic.
Claim. Let $r_μ := (gap(1332) - refined_shift) + step_{eμ}$. Then $-9.63 < r_μ < -9.62$.
background
In the T10 necessity module the lepton ladder is forced from the electron mass (T9) and geometric constants. The predicted muon residue is defined as (gap 1332 minus refined shift) plus step_e_mu, where step_e_mu equals E_passive plus 1/(4π) minus α². Upstream gap_minus_shift_bounds_proven supplies the interval (-20.7063, -20.705) for the gap term while step_e_mu_bounds supplies (11.079, 11.080) for the step. The module replaces two axioms in the lepton generations file with proven inequalities on the residues.
proof idea
The term proof unfolds the definition of predicted_residue_mu by simp, obtains the gap-shift bounds from gap_minus_shift_bounds_proven and the step bounds from step_e_mu_bounds, then applies constructor followed by linarith to combine the intervals.
why it matters
This lemma anchors the muon residue bounds that feed directly into phi_pow_residue_mu_lower, phi_pow_residue_mu_upper and the tau residue bounds. It forms part of the T10 necessity proof that the lepton ladder is forced by the eight-tick structure and phi self-similarity. The result closes one seam in the mass formula on the phi-ladder by providing explicit numerical control on the residue exponent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.