muon_mass_pred_bounds_proven
plain-language theorem explainer
The theorem establishes that the predicted muon mass lies strictly between 105 and 107 in Recognition Science units. Researchers deriving lepton hierarchies from the T9 electron mass would cite it to confirm the muon follows from structural scaling by a golden-ratio residue. The proof is a direct term application of the structural-mass interval and the phi-residue interval.
Claim. $105 < m_μ^{pred} < 107$, where $m_μ^{pred}$ is the electron structural mass multiplied by $φ$ raised to the muon residue power.
background
The electron structural mass equals $2^{-22} φ^{51}$ and is bounded in (10856, 10858) by the upstream structural_mass_bounds theorem, which rewrites the closed form and applies Fibonacci identities together with rational phi bounds. The predicted muon mass is obtained by multiplying this structural mass by $φ$ to the power of the muon residue, a quantity derived from the step function that combines passive cube edges (11), the fine-structure constant, and spherical geometry. This declaration sits inside the T10 module whose goal is to replace two earlier axioms by proving that the muon and tau masses are forced from the T9 electron mass plus the geometric constants E_passive = 11, cube faces = 6, wallpaper groups W = 17, and α.
proof idea
The proof is a one-line term that directly supplies the pair of bounds from the lower and upper lemmas for the predicted muon mass. Those lemmas are obtained by interval multiplication of the structural-mass bounds with the phi-power residue bounds for the muon step.
why it matters
This result replaces an axiom in the lepton-generations module and is invoked by the main T10 theorem lepton_ladder_forced_from_T9, which states that the muon mass is completely determined by the electron structural mass, passive edges, cube faces, wallpaper groups, and α. It thereby closes one link in the T9-to-T10 forcing chain, confirming that the phi self-similar fixed point and eight-tick octave propagate to the first lepton generation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.