muon_mass_pred_bounds_tight
plain-language theorem explainer
The declaration proves that the predicted muon mass satisfies 105.3 < m_pred < 106.5 in RS units. Researchers closing the lepton mass hierarchy from the electron structural scale and phi residues would cite it to complete the T10 necessity step. The proof is a direct term pairing of the module's lower and upper bound theorems.
Claim. The predicted muon mass, given by the electron structural mass multiplied by the golden ratio raised to the muon residue power, satisfies $105.3 < m_μ^{pred} < 106.5$.
background
In the T10 module the lepton ladder is forced from the electron structural mass (T9) together with cube-derived steps (E_passive = 11, W = 17) and the golden ratio phi (T4). The electron structural mass equals 2^{-22} * phi^{51} and is bounded by the upstream theorem structural_mass_bounds as 10856 < electron_structural_mass < 10858. The predicted muon mass is defined as electron_structural_mass * phi ^ predicted_residue_mu, where the residue encodes the geometric step for the first generation above the electron.
proof idea
The proof is a one-line term wrapper that pairs the lower bound theorem predicted_mass_mu_lower_tight with the upper bound theorem predicted_mass_mu_upper_tight.
why it matters
This theorem supplies the tight muon interval required to replace the axiomatic muon bound in LeptonGenerations.lean and thereby advance the T10 claim that the entire lepton ladder is forced by prior geometric constants. It sits downstream of structural_mass_bounds and the phi-ladder constructions, linking directly to the eight-tick octave and the self-similar fixed point phi in the T0-T8 chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.