step_mu_tau
plain-language theorem explainer
The step_mu_tau definition supplies the coefficient for the muon-to-tau transition in the lepton mass ladder. Researchers assembling Recognition Science mass predictions cite it when closing the e-mu-tau chain under geometric and symmetry constraints. It is a direct algebraic substitution of the three-dimensional cube face count together with the wallpaper group count scaled by the fine-structure constant.
Claim. The muon-to-tau step coefficient equals $6 - (37/2) alpha$, where 6 is the face count of the three-dimensional cube and the prefactor 37/2 arises from (2 times the wallpaper group count plus 3) divided by 2.
background
This definition sits in the T10 Lepton Generations Definitions module, which isolates core constants for lepton mass derivations to break import cycles. Cube faces returns twice the dimension, so cube_faces 3 equals 6. Wallpaper groups is the fixed crystallographic constant 17. Alpha is the fine-structure constant taken from the AlphaDerivation module. The local expression therefore combines the direct face term with a linear correction whose coefficient encodes wallpaper symmetry.
proof idea
One-line definition that substitutes the evaluated cube_faces 3 and the constant wallpaper_groups into the expression (cube_faces 3) minus ((2 * wallpaper_groups + 3) / 2) times alpha.
why it matters
The definition is referenced in forty downstream results inside JCostPerturbation, including the O4 channel closure certificate, the slot forcing certificate, and the explicit channel split theorem step_mu_tau_channel_split. It supplies the second link in the T10 lepton generation chain, using the D=3 spatial dimension and the alpha band to fix the tau mass relative to the muon. It thereby supports the claim that lepton masses are determined by geometric face counts and wallpaper symmetry factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.