predicted_mass_mu_upper
plain-language theorem explainer
The theorem proves the predicted muon mass lies strictly below 107 in Recognition Science units. Researchers deriving forced lepton hierarchies from the phi-ladder cite it when replacing axiomatic mass assumptions. The tactic proof rewrites the mass definition then multiplies the structural mass upper bound by the phi-residue upper bound via nlinarith and norm_num.
Claim. The structural electron mass multiplied by the golden ratio to the power of the predicted muon residue satisfies $m < 107$.
background
In the Recognition Science setting the lepton ladder is forced under T10 from the electron structural mass of T9 together with geometric steps. The structural mass equals the yardstick scaled by phi to the electron rung minus the octave period. The predicted muon mass is this quantity times phi raised to the residue that adds the gap, shift, and electron-muon step from cube geometry and alpha.
proof idea
The proof simplifies the predicted mass definition, obtains the structural mass bounds theorem and the phi-power residue upper bound theorem, then applies a calc block. nlinarith handles the product inequality 10858 * 0.0098 while norm_num confirms the final comparison to 107.
why it matters
This result supplies the upper half of the muon mass prediction bounds theorem that replaces an earlier axiom. It advances the T10 necessity claim by confirming the forced interval on the phi-ladder mass formula, consistent with the phi fixed point and eight-tick octave. The bound closes interval propagation for the yardstick * phi^(rung-8 + gap) expression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.