step_e_mu_bounds
plain-language theorem explainer
The geometric step from electron to muon mass satisfies 11.079 < step_e_mu < 11.080 in RS units. Researchers deriving forced lepton spectra from cube geometry and the fine-structure constant would cite this to anchor the muon residue. The proof reduces the definition via the exact passive-edge count then closes the resulting inequalities by linear arithmetic on the supplied bounds for 1/(4π) and α².
Claim. $11.079 < E_0 + 1/(4π) - α² < 11.080$ where $E_0 = 11$ is the exact count of passive cube edges.
background
In the T10 module the lepton ladder is forced from the electron mass (T9) by adding two geometric steps. The first step is defined as the sum of the passive-edge count E_passive, the spherical correction 1/(4π), and the subtraction of α². Upstream lemmas establish E_passive = 11 exactly, bound 1/(4π) inside (0.0795, 0.0796), and bound α² inside (0.0000532, 0.0000533). These constants originate from the cube geometry and eight-tick structure already derived in earlier modules.
proof idea
The term proof simplifies the definition of the step, rewrites the passive-edge term to its exact integer value, introduces the two numeric bound lemmas, and closes both sides of the conjunction by linear arithmetic.
why it matters
The lemma supplies the tight interval required by the downstream predicted-residue-mu-bounds result, which in turn feeds the RRF version of the same statement. It closes one concrete link in the T10 necessity argument that the muon and tau masses are determined by the same cube-derived constants (faces = 6, wallpaper groups = 17, α) that fix the electron mass. The result therefore belongs to the chain that replaces the original lepton axioms with proven inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.