tauStepCoefficientDerived_eq
plain-language theorem explainer
The declaration confirms that the tau generation step coefficient, defined as the sum of the wallpaper groups count and half the spatial dimension, evaluates exactly to 18.5. Researchers deriving lepton mass ladders in the Recognition Science framework cite it to anchor the (2W + 3)/2 factor in the muon-to-tau transition formula. The proof is a one-line term-mode reduction that unfolds the coefficient definition together with W, dim, D, and wallpaper_groups then normalizes the resulting arithmetic.
Claim. The derived coefficient satisfies $C_τ = W + D/2 = 18.5$, where $W = 17$ counts the distinct 2D wallpaper groups and $D = 3$ is the spatial dimension of the ledger.
background
The TauStepDerivation module derives the linear α-correction coefficient in the lepton generation step formula step_mu_tau = F − (2W + 3)/2 ⋅ α. The coefficient is introduced as the noncomputable definition C_τ = W + D/2, with W the number of 2D wallpaper groups and D the spatial dimension. Upstream results supply wallpaper_groups ≔ 17 (Fedorov 1891), the abbreviation W ≔ wallpaper_groups, and dim ≔ D.
proof idea
The term-mode proof unfolds tauStepCoefficientDerived, W, dim, D, and wallpaper_groups, then applies norm_num to reduce the concrete arithmetic 17 + 3/2 to the numeral 18.5.
why it matters
This verification closes the structural derivation of the (2W + 3)/2 term presented in the module documentation, showing it equals W + D/2 once D = 3 is inserted. It thereby grounds the muon-to-tau mass step in the wallpaper symmetry and dimensionality landmarks of the forcing chain rather than an arbitrary fit. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.