stepMuTauDerived
plain-language theorem explainer
The definition computes the muon-to-tau lepton generation step as the face count F minus the derived coefficient times the fine-structure constant alpha. Physicists modeling lepton mass hierarchies from wallpaper symmetry and spatial dimension in Recognition Science cite this for the explicit origin of the (2W+3)/2 prefactor. It is realized as a direct algebraic subtraction that invokes the precomputed tauStepCoefficientDerived.
Claim. $step_{mu tau} = F - (W + D/2) alpha$, where $F$ is the cube face count, $W$ the number of wallpaper groups, $D$ the spatial dimension, and $alpha$ the fine-structure constant.
background
The module derives the muon-to-tau step from first principles using wallpaper symmetry coupled to dimensionality. Face count F is defined as cube_faces D. Wallpaper groups W is the crystallographic constant for 2D symmetries. The coefficient is obtained from tauStepCoefficientDerived as (W : ℝ) + (dim : ℝ) / 2, which equals 37/2 when W=17 and D=3. Upstream, Constants.alpha supplies the fine-structure constant while AnchorPolicy.F and CellularAutomata.step provide the broader ledger and locality context.
proof idea
One-line definition that subtracts the product of tauStepCoefficientDerived and Constants.alpha from F.
why it matters
This definition supplies the explicit expression verified in the downstream theorem stepMuTauDerived_matches_def. It fills the structural derivation of the lepton generation coefficient from W + D/2, consistent with T8 forcing D=3 spatial dimensions and the Recognition Composition Law. It closes the gap between the paper formula step_mu_tau = F - (2W+3)/2 * alpha and the first-principles ingredients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.