step_e_mu_bounds
plain-language theorem explainer
The lemma establishes that the electron-muon step, defined as eleven passive cube edges plus the reciprocal of four pi minus alpha squared, lies strictly between 11.079 and 11.080. Researchers deriving forced lepton masses from the Recognition framework cite this interval to control the predicted muon residue. The argument reduces the expression by exact substitution of the edge count and applies linear arithmetic to the supplied bounds on the spherical correction and alpha squared.
Claim. Let $E_0=11$, let $step_{eμ}:=E_0+1/(4π)-α^2$, and let $α$ be the fine-structure constant. Then $11.079<step_{eμ}<11.080$.
background
In the lepton-generation necessity module the ladder from electron to muon is assembled from the structural electron mass together with geometric step functions. The electron-muon step is the sum of the passive edge count $E_0$, the spherical-geometry term $1/(4π)$, and the small correction $-α^2$. Upstream lemmas supply the exact identity $E_0=11$ together with tight interval bounds on both $1/(4π)$ and $α^2$ (the latter obtained from the already-proven alpha bounds).
proof idea
The proof is a direct term-mode reduction. It simplifies the definition of the step, rewrites the passive edge count to its exact value eleven, invokes the pre-established interval lemmas for the inverse-four-pi term and for alpha squared, then splits the conjunction and discharges both inequalities by linear arithmetic.
why it matters
The bound is invoked by the parent lemma predicted_residue_mu_bounds that assembles the muon residue from the gap-shift term and this step. It contributes to the T10 necessity argument that the lepton masses are forced once the electron mass and the cube-derived constants are fixed. The calculation rests on the wallpaper-group count, cube-face count, and the alpha band already constrained in earlier modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.