wallpaper_status
plain-language theorem explainer
The declaration records the classical result that exactly 17 wallpaper groups classify all two-dimensional periodic patterns. Crystallographers cite Fedorov's 1891 enumeration when enumerating lattice symmetries. The definition is a direct string assignment that tags the fact inside the axiom registry.
Claim. There exist exactly 17 distinct two-dimensional crystallographic groups.
background
The module maintains an axiom registry that separates physical postulates from well-known mathematical facts and open problems. Wallpaper groups count is entered as a standard result from Fedorov (1891) and Pólya (1924). Upstream, the Status inductive type tags entries as spec, derived, hypothesis or scaffold, while E counts the edges of the D-cube.
proof idea
One-line definition that binds the string constant to the identifier.
why it matters
This entry registers the 17 wallpaper groups as a mathematical fact within the Recognition Science axiom registry, supporting derivations in AlphaDerivation.lean. It aligns with the framework's reliance on standard group-theory results to constrain models in three dimensions. No open questions attach to this entry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.