step_mu_tau_bounds
plain-language theorem explainer
Step_mu_tau is bounded between 5.86 and 5.87, confirming the numerical stability of the muon-to-tau transition in the forced lepton spectrum. Mass hierarchy modelers cite this when verifying geometric predictions against observed tau mass. Algebraic reduction to alpha bounds followed by nlinarith closes the argument.
Claim. $5.86 < 6 - (2W + 3)/2 * alpha < 5.87$ where $W = 17$ is the wallpaper symmetry count and $alpha$ is the fine-structure constant.
background
The module proves T10 necessity: the lepton ladder is forced from the electron mass (T9) and geometric constants. Step functions combine cube faces (6), wallpaper groups (17), passive edges (11), and alpha, all derived from cube geometry and the eight-tick structure.
proof idea
The term proof simplifies the step_mu_tau definition, rewrites via cube_faces_exact and W_exact, obtains alpha_bounds, then applies constructor followed by nlinarith on both sides.
why it matters
It supplies the numerical step for predicted_residue_tau_bounds, which closes the tau residue interval and supports the full lepton mass prediction chain in T10. The result rests on alpha_bounds and the cube-derived constants from upstream modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.