orthorhombicConstraint
plain-language theorem explainer
The definition states that lattice parameters satisfy the orthorhombic constraint precisely when all three angles equal 90 degrees. Workers classifying the seven crystal systems under the Recognition Science derivation would cite it when checking the base symmetry for orthorhombic Bravais lattices. It is a direct equational definition consisting of a conjunction of three angle equalities.
Claim. For lattice parameters with lengths $a,b,c$ and angles $α,β,γ$, the orthorhombic constraint holds if and only if $α=β=γ=90^∘$.
background
LatticeParams is the structure recording the three edge lengths and three interaxial angles of a unit cell. The module derives the 32 point groups and 7 crystal systems from the 8-tick octave that forces three spatial dimensions together with the requirement that identical units tile space periodically without gaps. Only rotation orders 1, 2, 3, 4 and 6 are admissible; the orthorhombic case is the one in which three mutually perpendicular twofold axes are present.
proof idea
This is a direct definition that sets the orthorhombic constraint equal to the conjunction of the three right-angle conditions on the lattice angles.
why it matters
It supplies the minimal angle condition used by the downstream theorems cubic_most_constrained and tetragonal_implies_orthorhombic, which show that cubic and tetragonal constraints each imply the orthorhombic one. The declaration therefore participates in the enumeration of the seven crystal systems that the module obtains from the 8-tick structure and the crystallographic restriction. It contributes to the explicit count of exactly seven systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.