stepMuTauDerived
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 in Recognition Science
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.
scope and limits
- Does not derive numerical values of F or W from more primitive axioms.
- Does not compute actual lepton masses, only the step coefficient.
- Does not address electron or muon steps or higher generations.
- Does not incorporate quantum corrections beyond the alpha term.
Lean usage
rw [stepMuTauDerived]formal statement (Lean)
93noncomputable def stepMuTauDerived : ℝ :=
proof body
Definition body.
94 (F : ℝ) - tauStepCoefficientDerived * Constants.alpha
95
96/-- Main Theorem: The derived step matches the definition in Defs.lean. -/