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

wallpaper_groups

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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).

scope and limits

Lean usage

theorem seam_example : seam_denominator 3 = 102 := rfl

formal statement (Lean)

  78def wallpaper_groups : ℕ := 17

proof body

Definition body.

  79
  80/-- Face-wallpaper pairs. -/

used by (40)

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

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.