pith. machine review for the scientific record. sign in
def definition def or abbrev high

W

show as:
view Lean formalization →

W is the integer constant set to the number of distinct two-dimensional wallpaper groups. Lepton mass derivations in Recognition Science cite this value when assembling the coefficient (2W + 3)/2 for the muon-to-tau step. The definition is a direct one-line alias to the upstream crystallographic constant.

claim$W = 17$, the number of distinct 2D wallpaper groups in the Euclidean plane.

background

The module derives the tau generation step from wallpaper symmetry on cube faces coupled to spatial dimension. Wallpaper groups are the 17 distinct 2D symmetry classes classified by Fedorov in 1891. The definition imports this constant from AlphaDerivation.wallpaper_groups and MassTopology.W, where it is fixed at 17 and described as the count of face symmetries.

proof idea

One-line definition that directly aliases wallpaper_groups from the AlphaDerivation module.

why it matters in Recognition Science

This supplies the W=17 that produces the coefficient C_τ = W + D/2 = 18.5 in the muon-to-tau formula, matching (2W + 3)/2 exactly. It parametrizes the window length in the canonical recognition cost system of CostAlgebra and traces to the T8 forcing of D=3 together with 2D face mediation in the mass topology.

scope and limits

formal statement (Lean)

  67def W : ℕ := wallpaper_groups

proof body

Definition body.

  68
  69/-- Spatial dimension. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.