hexagonalConstraint
plain-language theorem explainer
The hexagonalConstraint definition encodes the lattice parameters for the hexagonal crystal system. A solid-state physicist or crystallographer working from Recognition Science would cite it when enumerating the seven systems that arise from space-filling constraints in three dimensions. It is realized as a direct conjunction of four equalities on the six lattice parameters.
Claim. A lattice with edge lengths $a,b,c$ and angles $α,β,γ$ satisfies the hexagonal constraint when $a=b$, $α=90^∘$, $β=90^∘$, and $γ=120^∘$.
background
LatticeParams records the three edge lengths and three inter-edge angles of a unit cell. The module derives the seven crystal systems from the Recognition Science 8-tick structure, which forces three spatial dimensions and restricts rotational symmetries to orders 1, 2, 3, 4, 6 so that identical units can tile space periodically without gaps. Upstream constants such as the fine-structure constant and Euler-Mascheroni γ appear in the module imports but enter only at the level of the broader constant framework.
proof idea
The definition is a direct abbreviation consisting of the four equalities that fix the hexagonal system.
why it matters
This definition supplies one of the seven crystal systems required by the module's derivation of the 32 crystallographic point groups from the 8-tick octave and the space-filling restriction. It supports the explicit count of exactly seven systems and fourteen Bravais lattices stated in the module documentation. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.