wallpaper_groups
plain-language theorem explainer
The definition assigns the integer 17 to the count of distinct two-dimensional wallpaper groups. A physicist constructing the fine-structure constant from D=3 cubic ledger geometry cites this value to form the seam denominator 102 in the curvature fraction. The assignment imports the 1891 Fedorov classification as a fixed crystallographic input without internal derivation from the Recognition axioms.
Claim. The number of distinct two-dimensional wallpaper groups is $17$.
background
The Alpha Derivation module starts from the Meta-Principle forcing a discrete ledger on Z³ whose unit cell is the cube Q₃. For D=3 this cube has 6 faces, 12 edges and 8 vertices. One edge is traversed per atomic tick, leaving 11 passive edges whose coupling to vacuum geometry supplies the curvature terms. The module normalizes these terms by the product of face count and the number of 2D wallpaper groups, yielding the base denominator 102 plus one Euler closure to reach the seam count 103.
proof idea
The definition is a direct constant assignment of the Fedorov number 17. No lemmas or tactics are invoked; the value is supplied as a primitive input to the normalization calculations performed by seam_denominator and alpha_ingredients_from_D3_cube.
why it matters
This definition supplies the crystallographic constant required for seam_denominator D = cube_faces D * wallpaper_groups, which equals 102 for D=3 and appears in the geometric seed factor and curvature numerator of the alpha derivation. It is referenced by AlphaFrameworkCert and delta_1_neg, closing the D=3 cube geometry that links the Recognition forcing chain (T8) to the observed alpha band. The value is treated as an external crystallographic fact rather than derived from J-cost or phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.