muon_mass_pred_bounds
plain-language theorem explainer
The declaration proves that the Recognition Science predicted muon mass lies strictly between 105 and 107 MeV. Researchers checking consistency of the passive field step with observed lepton masses would cite this bound. The proof is a direct one-line application of the interval propagation result from the Necessity submodule.
Claim. $105 < m_μ^{pred} < 107$, where $m_μ^{pred}$ is the muon mass obtained from the structural mass multiplied by $φ$ to the power of the muon residue.
background
The Lepton Generations module derives higher-generation lepton masses by extending the topological ladder from the electron. The mass formula is $m_n = m_{struct} · φ^{Δ_n}$, with the muon residue obtained by adding the passive field step $S_{e→μ} = 11 + 1/(4π) - α² ≈ 11.07952$ to the electron residue. Upstream results include the structural mass definition and the necessity theorem that propagates interval bounds from the phi-residue to the final mass prediction.
proof idea
This is a one-line term proof that directly invokes the necessity theorem muon_mass_pred_bounds_proven, which supplies the lower and upper bounds via the structural mass and phi-residue interval propagation.
why it matters
The result supplies the proven bounds required by the downstream muon mass step hypothesis to verify that the relative error stays below 2 percent for the passive field step. It completes the T10 muon generation step in the lepton chain, connecting to the phi-ladder mass formula and the eight-tick octave structure of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.