stepMuTauDerived_matches_def
plain-language theorem explainer
The theorem confirms that the derived muon-to-tau generation step equals the explicit formula F minus (2W plus 3) over 2 times alpha, where F counts cube faces and W counts wallpaper groups. Physicists modeling lepton mass ladders in Recognition Science cite it to anchor the coefficient in geometric symmetry rather than fitting. The proof rewrites the input equality, unfolds the derived step, and reduces via the coefficient matching result.
Claim. Let $step = F - (2W + 3)/2 * alpha$, where $F$ is the face count and $W$ the wallpaper group count. Then the derived muon-to-tau step equals this $step$.
background
This module derives the muon-to-tau step from wallpaper symmetry and spatial dimension. The target formula is step_mu_tau = F - (2W + 3)/2 * alpha. The coefficient (2W + 3)/2 expands as W + D/2 with D the spatial dimension. Upstream, F is defined as cube_faces D and W as wallpaper_groups. Constants.alpha supplies the fine-structure constant as 1/alphaInv. The module doc states that the coefficient arises because the transition is face-mediated and therefore couples to the 17 wallpaper groups plus half the dimension.
proof idea
The proof rewrites the supplied hypothesis into the target equality. It then unfolds stepMuTauDerived, which subtracts tauStepCoefficientDerived times alpha from F. The final rewrite applies tauStepCoefficientDerived_matches_paper to complete the reduction.
why it matters
The result closes the structural derivation of the tau coefficient inside the lepton generations module, confirming it matches the definition supplied in Defs.lean. It grounds the alpha correction in T8 (D = 3) and the wallpaper count W = 17, consistent with the Recognition Science forcing chain that produces mass steps on the phi-ladder. No downstream theorems are listed, so the declaration serves as a terminal matching step rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.