step_mu_tau_bounds_v2
plain-language theorem explainer
The muon-to-tau step function is shown to lie strictly between 5.8649 and 5.8651. Workers closing the T10 lepton-ladder necessity argument cite the bound to confirm that the second mass ratio is fixed once D=3, W=17 and the alpha interval are in place. The term proof substitutes the exact constants for faces, wallpaper groups and D, then closes both sides of the target inequality with nlinarith on the alpha bounds.
Claim. $5.8649 < s < 5.8651$ where $s = 6 - (2W + D)/2 · α$, $D=3$, $W=17$ and $0.007297 < α < 0.0072977$.
background
Module T10 replaces the two lepton-generation axioms with proven mass bounds once the electron mass (T9) and the geometric constants are fixed. step_mu_tau is defined as (cube_faces D) minus (2·wallpaper_groups + D)/2 times alpha; cube_faces D evaluates to 6 for D=3. Upstream lemmas supply the remaining pieces: W_exact fixes wallpaper_groups = 17, alpha_bounds supplies the narrow interval on the fine-structure constant, and the two cube_faces definitions confirm the face count 2D.
proof idea
Term-mode proof. simp unfolds step_mu_tau and replaces W, D and cube_faces by their exact values. The alpha interval is obtained by have h_alpha := alpha_bounds. constructor splits the conjunction and nlinarith closes both resulting inequalities.
why it matters
The lemma supplies the numerical control required by predicted_residue_tau_bounds_v2, which in turn bounds the tau residue. It therefore advances the T10 program of deriving the entire lepton ladder from T9 plus the cube geometry (D=3, faces=6) and wallpaper count (W=17) already established upstream. The result sits inside the forcing chain that begins with T5 J-uniqueness and T8 spatial dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.