step_e_mu_bounds_v2
plain-language theorem explainer
The lemma establishes that the electron-to-muon step function equals 11 plus 1 over 4π minus α squared and lies strictly between 11.0795 and 11.0796. Researchers deriving forced muon and tau masses from the electron structural mass and cube geometry would cite this interval. The proof is a short term-mode reduction that substitutes the exact passive edge count, invokes the supplied bounds on 1 over 4π and on α squared, then closes both sides of the conjunction with linear arithmetic.
Claim. $11.0795 < 11 + 1/(4π) - α² < 11.0796$
background
In the T10 module the lepton ladder is forced from the electron structural mass (T9) together with cube geometry and the fine-structure constant. The step function is defined as E_passive plus 1 over 4π minus α squared, where E_passive counts the passive edges of the cube. Upstream lemmas supply the exact value E_passive = 11, the strict interval 0.07957 < 1/(4π) < 0.07958, and the interval 0.0000532 < α² < 0.0000533.
proof idea
The proof unfolds the definition of the step via simp, rewrites E_passive to its exact value 11, obtains the lower and upper bounds on 1/(4π) and on α² from the cited lemmas, then applies constructor to split the conjunction and closes both sides with linarith.
why it matters
This lemma supplies the numerical interval required by the subsequent bound on the muon residue. It forms part of the T10 necessity argument that the lepton masses are completely determined by the electron mass, the passive edge count 11, cube faces 6, wallpaper groups 17, and α. Within the framework it closes one link in the forcing chain from T9 to the full lepton spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.