tetragonalConstraint
plain-language theorem explainer
The tetragonalConstraint encodes the geometric conditions for the tetragonal crystal system on a LatticeParams record: equal a and b edge lengths together with three right angles. Derivations of the seven crystal systems from 3D space-filling rules cite this definition to classify lattices by symmetry. It is realized as a direct conjunction of equalities on the record fields.
Claim. For lattice parameters $p$, the tetragonal constraint holds precisely when $p.a = p.b$ and the angles satisfy $p.alpha = p.beta = p.gamma = 90^circ$.
background
LatticeParams is the structure that records three positive edge lengths a, b, c together with the three inter-edge angles alpha (between b and c), beta (between a and c), and gamma (between a and b). The module places this structure inside the Recognition Science derivation of crystal symmetry from the 8-tick octave, which forces three spatial dimensions and restricts periodic tilings to rotation orders 1, 2, 3, 4, and 6. Upstream results supply the raw LatticeParams definition and the auxiliary constants (alpha, gamma, beta) that appear in neighboring modules but are not invoked inside this particular definition.
proof idea
The declaration is a one-line definition that directly assembles the required conjunction of equalities on the four fields of the input LatticeParams record.
why it matters
The definition is invoked by the downstream theorem tetragonal_implies_orthorhombic, which shows that every tetragonal lattice also satisfies the orthorhombic constraints. It therefore participates in the module's enumeration of the seven crystal systems that arise once the 8-tick structure has fixed D = 3 and the crystallographic restriction has eliminated 5-fold and 7-fold rotations. The surrounding module doc-comment records the explicit prediction of exactly seven crystal systems and fourteen Bravais lattices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.