Verification Wallpaper Classification Bridge

The Cube's Wallpaper

Wallpaper patterns are the repeating designs that cover a flat surface without gaps or overlaps. In 1891, the Russian crystallographer Evgraf Fedorov proved that there are exactly 17 distinct symmetry types for such patterns, known as the wallpaper groups. Each group describes a different combination of translations, rotations, reflections, and glide reflections that can repeat forever in two dimensions. The 17 groups are a classical result of geometry, taught in crystallography and group theory courses worldwide.

The wallpaper groups split naturally by the shape of the repeating lattice. Two groups work on an oblique lattice, seven on a rectangular one, three on a square lattice, and five on a hexagonal lattice. The square groups include p4, p4m, and p4g, which describe patterns like those on a checkerboard or a tiled bathroom floor. The hexagonal groups include p3, p3m1, p31m, p6, and p6m, which describe patterns like those in a honeycomb. Each group's name is a standard crystallographic label, and the count of 17 is a theorem that any modern proof assistant can verify by simple enumeration.

In Recognition Science, the framework asks whether this classical list of 17 can be derived from the internal structure of a three-dimensional cube. The framework models a cube as having six square faces and twelve edges. Its machine-checked library of formal theorems proves that the cube's face symmetries, the rotations and reflections that leave a face in place, form the dihedral group D₄ of order 8. This point group is compatible with the oblique, rectangular, and square lattice types, accounting for 12 of the 17 wallpaper groups. The remaining five hexagonal groups arise from the triangular decomposition of each square face, which connects to the icosahedron's 12 triangular facets.

The central theorem of the module is a structural decomposition: the 17 wallpaper groups equal the sum of 11 edge-generated groups and 6 face-generated groups. The 11 edge groups come from one-dimensional symmetries like translations and reflections along the cube's passive edges. The 6 face groups come from two-dimensional rotational symmetries of the cube's faces. The theorem W_decomposition proves this equality, and W_eq_17 shows the sum equals 17. The module also classifies each of the 17 groups by its dominant symmetry type, proving that exactly 11 are edge-dominant and 6 are face-dominant.

This decomposition is not a coincidence but a reflection of the cube's combinatorial structure. The count W = E_passive + F equals 17 only when the dimension D equals 3, which the module proves in WallpaperEndogenousBridge.lean. In plain language, the cube's six faces and twelve edges provide a reason why there are exactly 17 wallpaper patterns, not 16 or 18. The assignment of each group to an edge or face type is currently a definition based on standard crystallography, not a derivation from first principles. The module leaves open the task of defining edge-type and face-type generators purely from the cube's combinatorial structure, which would make the bridge fully endogenous.

/-- The structural decomposition: W = edge_generated + face_generated. -/
theorem W_decomposition :
    edge_generated_groups + face_generated_groups = wallpaper_groups := by
  native_decide

/-- This equals the classical count of 17 wallpaper groups. -/
theorem W_eq_17 :
    edge_generated_groups + face_generated_groups = 17 := by
  native_decide

/-- 11 groups are edge-dominant. -/
theorem edge_dominant_eq_Ep : edge_dominant_count = 11 := by native_decide

/-- 6 groups are face-dominant. -/
theorem face_dominant_eq_F : face_dominant_count = 6 := by native_decide

/-- There are exactly 17 wallpaper groups. -/
theorem wallpaper_group_count : Fintype.card WallpaperGroup = 17 := by native_decide

What this page does not claim

The assignment of each wallpaper group to an edge or face type is not derived from first principles; it is a definition based on the standard classification. The module does not prove that the cube's structure generates the wallpaper groups; it only proves the count decomposition. The framework does not claim that wallpaper patterns physically exist in nature; it only shows a structural correspondence.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/WallpaperClassificationBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: