step_mu_tau_scale_forced
plain-language theorem explainer
The theorem shows that matching the canonical step_mu_tau expression to the form F minus ((2W + D)/c) alpha with c positive forces c exactly equal to 2. Lepton-mass modelers in Recognition Science cite it when closing the O4 perturbative channel for the mu-tau rung. The proof equates the two expressions for step_mu_tau, cancels the nonzero alpha factor via mul_right_cancel, reduces the numerator to 37, and solves the resulting proportion by cross-multiplication and nlinarith.
Claim. Let $F = 2D$ be the number of faces of the $D$-cube, $W = 17$ the number of wallpaper groups, and $alpha$ the fine-structure constant. If the real-scale mu-to-tau step satisfies $step_{mu tau} = F - ((2W + D)/c) alpha$ with $c > 0$, then $c = 2$.
background
The module supplies the J-cost perturbation bridge that ties lepton steps to the canonical O4 closure. cube_faces(D) evaluates to 2D and equals 6 when D=3. wallpaper_groups is the crystallographic constant 17. alpha is the fine-structure constant 1/alphaInv. step_mu_tau_channel_split supplies the explicit decomposition step_mu_tau = 6 - (37/2) alpha that the proof imports as the canonical target.
proof idea
The tactic proof first rewrites step_mu_tau via step_mu_tau_channel_split and norm_num to obtain the canonical 6 - (37/2)alpha form. It then equates the two expressions for step_mu_tau, cancels the positive alpha factor with mul_right_cancel, reduces the coefficient (2W + D)/c to 37/2, and solves the resulting proportion (37/c = 37/2) by cross-multiplication and nlinarith.
why it matters
This declaration closes the real-scale denominator forcing inside the J-cost perturbation layer and feeds the lepton-mass ladder used by downstream mass-topology counts. It directly instantiates the O4 coefficient-forcing program described in the module doc-comment. The result relies on the alpha band and the D=3 geometry already fixed by the forcing chain T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.