predicted_residue_mu_bounds_v2
plain-language theorem explainer
The lemma establishes that the predicted muon residue lies strictly between -9.6268 and -9.6254. Researchers deriving forced lepton masses from the Recognition Science ladder cite this interval to anchor the muon step. The proof unfolds the residue definition then combines independent bounds on the gap-shift term and the electron-muon step via linear arithmetic.
Claim. $-9.6268 < (gap(1332) - refined_shift) + step_{eμ} < -9.6254$
background
In the T10 Necessity module the lepton ladder is forced from the T9 electron mass together with cube geometry and the golden ratio. The predicted muon residue is defined as (gap 1332 minus refined shift) plus step e mu, where the gap term encodes the RS gap function evaluated at rung 1332 and the step encodes the transition via passive edges and fine-structure contributions.
proof idea
Unfold the definition of predicted_residue_mu by simp. Obtain the gap-shift interval from gap_minus_shift_bounds_proven and the step interval from step_e_mu_bounds_v2. Split the conjunction with constructor and close both inequalities by linarith.
why it matters
The bounds feed directly into phi_pow_residue_mu_lower_v2 and phi_pow_residue_mu_upper_v2, which verify the phi-power residue interval, and into predicted_residue_tau_bounds_v2. It advances the T10 replacement of axioms by theorems, linking T9 electron mass, T6 phi and alpha, E_passive = 11, faces = 6, and W = 17 from cube and wallpaper geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.