step_mu_tau_channel_split
plain-language theorem explainer
Muon-to-tau lepton step equals six minus thirty-seven halves times the fine-structure constant. Lepton mass modelers in Recognition Science cite this explicit geometric form for the canonical mu-tau channel. The proof substitutes the pre-forced linear coefficient and evaluates the three-cube face count to six.
Claim. $step_{mu to tau} = 6 - (37/2) alpha$, where the constant term is the face count of the three-dimensional cube and the coefficient is fixed by the wallpaper-group normalization in the linear-alpha family.
background
The module supplies the J-cost perturbation bridge to canonical lepton steps. Alpha is the fine-structure constant. Cube faces equal twice the spatial dimension, hence six when the dimension is three. Wallpaper groups total seventeen by Fedorov's crystallographic classification. The muon-to-tau step belongs to the linear perturbation family in alpha; upstream results supply the alpha definition and the geometric counts used here.
proof idea
The proof first invokes the lemma that fixes the linear coefficient at thirty-seven over two. It then normalizes the cube face count to six by direct evaluation. A calc block substitutes both values into the step definition to reach the target expression.
why it matters
This closed form is required by the O4 channel closure certificate that assembles the full lepton hierarchy with radiative corrections. It underpins the denominator, scale, and joint Diophantine forcing theorems for the mu-tau channel. The result realizes the three-dimensional geometry and linear-alpha term in the Recognition mass ladder on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.