step_mu_tau
plain-language theorem explainer
step_mu_tau defines the numerical coefficient for the muon-to-tau lepton mass step as the hypercube face count minus a wallpaper-symmetry term scaled by alpha. Mass hierarchy derivations in Recognition Science cite it when assembling the full e-mu-tau chain from geometric inputs. The definition is a direct algebraic substitution of cube_faces D and wallpaper_groups into the supplied linear expression.
Claim. The muon-to-tau generation step coefficient equals $2D - ((2W + D)/2) alpha$, where $D=3$ is the number of spatial dimensions, $W=17$ is the number of two-dimensional wallpaper groups, and $alpha$ is the fine-structure constant.
background
Recognition Science isolates lepton mass steps in the T10 module to break import cycles while deriving successive generation coefficients from hypercube geometry and crystallographic symmetry. cube_faces(D) returns the face count 2D of the D-hypercube. wallpaper_groups returns the fixed crystallographic constant 17 from Fedorov 1891. The local expression combines these with the fine-structure constant alpha under the D=3 convention from the forcing chain.
proof idea
Direct definition. It substitutes the upstream cube_faces D (equal to 2D) and wallpaper_groups (equal to 17) into the explicit linear form (cube_faces D) - ((2 * wallpaper_groups + D)/2) * alpha, with D instantiated to 3.
why it matters
This supplies the canonical mu-to-tau coefficient required by downstream JCostPerturbation results including step_mu_tau_channel_split, o4_channel_closure_certificate, and lepton_real_scale_iff_bundle_no_hc_pos. It completes the T10 lepton chain step that links the eight-tick octave and D=3 spatial dimensions to the full family forcing certificates without positivity hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.