hexagonalConstraint
plain-language theorem explainer
hexagonalConstraint specifies the metric constraints for the hexagonal crystal system. Researchers enumerating the seven crystal systems from Recognition Science space-filling rules would cite this definition when classifying lattices. The declaration is a direct equational definition of the required equalities on lengths and angles.
Claim. For lattice parameters $p$, the hexagonal constraint is the proposition $p.a = p.b$, $p.alpha = 90$, $p.beta = 90$, $p.gamma = 120$.
background
LatticeParams is the structure holding the three edge lengths $a$, $b$, $c$ and the three angles alpha (between $b$ and $c$), beta (between $a$ and $c$), gamma (between $a$ and $b$). The module derives crystal symmetry from the 8-tick structure that forces three spatial dimensions and restricts periodic tilings to rotation orders 1, 2, 3, 4, 6. Hexagonal belongs to the list of seven systems obtained by clustering the 32 point groups according to their essential symmetry elements.
proof idea
Direct definition that states the four equality conditions on the components of LatticeParams.
why it matters
The definition supplies one of the seven crystal-system predicates used to reach the module's count of exactly seven systems and fourteen Bravais lattices. It implements the hexagonal case (one 6-fold axis) listed in the module documentation under the space-filling constraint that follows from the 8-tick octave. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.