essentialSymmetry
plain-language theorem explainer
The declaration defines a function that assigns to each of the seven crystal systems its minimal symmetry element required by periodic space-filling in three dimensions. Recognition Science researchers or crystallographers would cite it when partitioning the 32 point groups according to the crystallographic restriction. The definition proceeds by exhaustive case analysis on the CrystalSystem inductive type, returning a fixed string for each constructor.
Claim. Let $C$ denote the set of seven crystal systems. The essential symmetry map $s: C → String$ is given by $s( triclinic ) =$ ``none (or only 1-fold / inversion)'', $s( monoclinic ) =$ ``one 2-fold axis or mirror'', $s( orthorhombic ) =$ ``three perpendicular 2-fold axes'', $s( tetragonal ) =$ ``one 4-fold axis'', $s( trigonal ) =$ ``one 3-fold axis'', $s( hexagonal ) =$ ``one 6-fold axis'', and $s( cubic ) =$ ``four 3-fold axes (body diagonals)''.
background
Crystal symmetry emerges in Recognition Science from the 8-tick octave that forces three spatial dimensions. Any periodic arrangement of identical units must respect the underlying ledger geometry, which restricts rotational symmetries to orders 1, 2, 3, 4, and 6. The seven crystal systems therefore cluster the 32 crystallographic point groups by their essential symmetry elements: triclinic carries none, monoclinic carries one 2-fold axis or mirror, orthorhombic carries three perpendicular 2-fold axes, tetragonal carries one 4-fold axis, trigonal carries one 3-fold axis, hexagonal carries one 6-fold axis, and cubic carries four 3-fold axes along body diagonals.
proof idea
The definition is a direct pattern match on the seven constructors of the CrystalSystem inductive type. Each case returns the corresponding string literal that describes the minimal symmetry element for that system.
why it matters
This definition supplies the explicit descriptors that realize the clustering of point groups into the seven crystal systems predicted by the space-filling constraint. It implements the fourth step of the RS mechanism in the module documentation, connecting the 8-tick geometry and D = 3 directly to observable crystal classes. The declaration supports the module-level predictions of exactly seven crystal systems and exactly 32 point groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.