wallpaper_groups
plain-language theorem explainer
The declaration assigns the integer 17 to the number of distinct two-dimensional wallpaper groups, the crystallographic constant established by Fedorov in 1891. Derivations of higher-order corrections to the fine-structure constant in Recognition Science cite this value when forming the seam denominator on the D=3 cube. The definition is a direct constant assignment that matches the upstream crystallographic fact without further computation.
Claim. The number of distinct two-dimensional wallpaper groups is $17$.
background
The module formalizes higher-order voxel-seam corrections to α^{-1} within Recognition Science, building on the three-ingredient derivation of the fine-structure constant: geometric seed, gap weight, and curvature corrections δ_n. Central definitions include Q3_faces = 6 for the cube and seam_denominator d = cube_faces d × wallpaper_groups, which normalizes the curvature fraction. The upstream result in AlphaDerivation records the same assignment and notes that 6 × 17 yields the denominator 102 appearing in δ_1 = -103/(102 π^5).
proof idea
The definition is a direct constant assignment of the integer 17, inheriting its value from the upstream crystallographic constant in AlphaDerivation.
why it matters
This supplies the crystallographic factor required by alpha_ingredients_from_D3_cube, which proves that all numerical ingredients in the α^{-1} formula arise from D=3 cube geometry, and by seam_denominator, which sets the base normalization for the curvature series. It is recorded inside the AlphaFrameworkCert structure as one of the structural elements needed before δ_2 can be computed. The definition therefore closes a prerequisite for the alternating convergent series that targets the CODATA value 137.035999206(11).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.