wallpaper_groups_count
plain-language theorem explainer
The declaration records the established fact that exactly seventeen wallpaper groups tile the Euclidean plane. A researcher computing the fine-structure constant from cubic ledger geometry cites this integer to form the normalization 6 × 17 = 102 that enters the seam count. The proof is a direct reflexivity on the numeral seventeen that registers the crystallographic constant without internal derivation.
Claim. The Euclidean plane admits exactly seventeen distinct wallpaper groups under the action of rotations, reflections, and translations.
background
The Alpha Derivation module constructs α⁻¹ from the geometry of the cubic ledger Q₃ in D = 3. This ledger has six faces; during each atomic tick one edge is active while the remaining eleven are passive. The module closes the curvature calculation by multiplying the face count by the number of wallpaper groups to reach the base normalization 102, then adds the Euler +1 to obtain the seam count 103 that appears in the term 103/(102 π⁵).
proof idea
The proof is a term-mode reflexivity (rfl) that equates the numeral 17 with itself. No upstream lemmas are invoked; the declaration simply embeds the standard crystallographic count of seventeen groups as a fixed integer constant.
why it matters
This supplies the integer 17 required for the crystallographic closure step inside the alpha derivation: six faces times seventeen groups yields the base 102 used to normalize the geometric seed 4π · 11. It links the discrete cubic ledger (D = 3, six faces) to the classical classification of plane symmetry groups. The result completes the normalization that feeds the curvature term in the overall derivation of α⁻¹.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.