predicted_mass_mu_lower_tight
plain-language theorem explainer
The theorem proves a strict lower bound of 105.3 on the predicted muon mass in Recognition Science units. Physicists deriving forced lepton spectra from the phi-ladder would cite it to confirm consistency with the electron structural mass. The short tactic proof unfolds the mass definition then chains the structural mass lower bound with the phi-residue power lower bound via a numerical calc and nlinarith.
Claim. $105.3 < m_μ^{pred}$, where $m_μ^{pred} = m_{struct} ⋅ φ^{r_μ}$, $m_{struct}$ is the electron structural mass (lepton yardstick times $φ$ to the power of electron rung minus octave period), and $r_μ$ is the predicted muon residue (gap(1332) minus refined shift plus step_e_mu).
background
The module establishes T10 necessity: the lepton ladder is forced from T9 electron mass results together with cube geometry constants (E_passive = 11, faces = 6, W = 17) and the golden ratio φ from T4-T6. The electron structural mass is the dimensionless scale $m_{struct} = Y ⋅ φ^{r-8}$ (with $Y$ the lepton yardstick), proven in structural_mass_bounds to satisfy $10856 < m_{struct} < 10858$. The predicted muon mass is defined as $m_{struct} ⋅ φ^{r_μ}$ with residue $r_μ = (gap(1332) - refined_shift) + step_e_mu$. The companion lemma phi_pow_residue_mu_lower supplies the strict inequality $0.0097 < φ^{r_μ}$.
proof idea
The tactic proof first applies simp to unfold predicted_mass_mu into the product form. It obtains the structural mass lower bound via structural_mass_bounds and the phi-power lower bound via phi_pow_residue_mu_lower. A calc block uses norm_num to verify the concrete inequality 105.3 < 10856 * 0.0097, then nlinarith combines the two imported bounds to finish the goal.
why it matters
The result is the lower half of muon_mass_pred_bounds_tight, which tightens the predicted muon interval to (105.3, 106.5). It directly supports the module goal of replacing lepton axioms with proven inequalities derived from electron structural mass and geometric steps. Within the Recognition Science chain it relies on the phi self-similar fixed point (T6) and eight-tick octave (T7) that fix the residue exponents; no open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.