tauStepCoefficientDerived_matches_paper
plain-language theorem explainer
The coefficient in the muon-to-tau lepton generation step equals (2W + 3)/2 where W counts the wallpaper groups. Physicists deriving lepton mass ratios from symmetry would cite this to anchor the linear alpha correction. The proof unfolds the coefficient definition along with the dimension and normalizes the resulting expression algebraically.
Claim. The derived coefficient $C_τ$ in the muon-to-tau step satisfies $C_τ = (2W + 3)/2$, where $W$ is the number of wallpaper groups and the spatial dimension is fixed at 3.
background
The module derives the linear correction coefficient in the generation step formula step_mu_tau = F - C_τ α. Here F is the face count (6), W is the wallpaper group count (17) encoding 2D symmetries on the mediating faces, and D is the spatial dimension (3). The coefficient is obtained as C_τ = W + D/2, which rearranges exactly to (2W + 3)/2. Upstream results supply the generation type as a finite set of size 3 from SpectralEmergence and the anchor W from Masses.Anchor.
proof idea
The term-mode proof unfolds tauStepCoefficientDerived together with dim and D, then applies ring normalization to obtain the target algebraic form.
why it matters
This equality supplies the exact coefficient used by the downstream theorem stepMuTauDerived_matches_def, which in turn confirms the full step formula matches the paper definition. It closes the structural link between wallpaper symmetry, the fixed dimension D = 3 from the forcing chain, and the alpha correction in lepton masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.