tauStepCoefficientDerived
plain-language theorem explainer
The tau step coefficient is defined as the sum of the wallpaper group count and half the spatial dimension. Researchers constructing lepton generation steps from symmetry and dimensionality principles cite this when building the linear alpha correction for the muon-to-tau transition. The definition is introduced as a direct arithmetic expression combining the imported constants W and dim.
Claim. The tau step coefficient is defined by $C_τ = W + D/2$, where $W$ is the number of wallpaper groups and $D$ is the spatial dimension.
background
This definition sits inside the module that derives the tau generation step from wallpaper symmetry coupled to dimensionality. The module states that the coefficient in the step_mu_tau formula arises because the transition is face-mediated, coupling to the 17 wallpaper groups for 2D symmetries together with the spatial dimension of the ledger. The ingredients listed are faces F=6, wallpaper groups W=17, and dimension D=3, yielding the linear alpha-correction coefficient C_τ = W + D/2.
proof idea
The definition is a one-line wrapper that casts W to reals and adds half of dim. It directly applies the sibling definitions of W as wallpaper_groups and dim as D without additional lemmas or tactics.
why it matters
The coefficient is used in the downstream definition stepMuTauDerived that subtracts tauStepCoefficientDerived times alpha from F. It is verified to equal 18.5 and to match the paper form (2W + 3)/2 by the sibling theorems tauStepCoefficientDerived_eq and tauStepCoefficientDerived_matches_paper. In the framework it incorporates the spatial dimension D=3 from the forcing chain T8 together with the wallpaper symmetry count W=17 as a topological constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.