W
plain-language theorem explainer
W aliases the integer 17 as the count of two-dimensional wallpaper groups. Mass topology derivations in Recognition Science cite it for the base symmetry contribution to the electron ledger fraction. The definition is a direct alias to the Fedorov crystallographic constant.
Claim. Let $W = 17$ denote the number of distinct two-dimensional wallpaper groups.
background
The module Physics.MassTopology constructs the refined ledger fraction for the electron mass shift under T9 topology. It assembles the shift from the cubic ledger $Q_3$ geometry using base counts and radiative corrections, with the explicit formula involving $W$, $E_{total}$, $E_{passive}$, and powers of the fine-structure constant.
proof idea
One-line definition that directly aliases the wallpaper_groups constant imported from AlphaDerivation.
why it matters
W supplies the window length parameter to RecognitionCostSystem and canonicalRecognitionCostSystem in CostAlgebra, enabling the cost functional and its reciprocal and unit properties. It provides the base term $2W$ in the T9 ledger fraction, which matches empirical shifts to $2 times 10^{-7}$. The value originates from the Fedorov enumeration and supports the face symmetry cover required by the D=3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.