cubic_most_constrained
plain-language theorem explainer
Any lattice parameters satisfying the cubic constraints also satisfy the orthorhombic constraints. Crystallographers classifying systems by symmetry hierarchy would cite this when ordering the seven crystal systems. The proof is a direct term extraction that discards the length equalities from the cubic hypothesis and returns only the three right-angle conditions.
Claim. For all lattice parameters $p$, if $a=b=c$ and all angles equal $90^circ$, then all angles equal $90^circ$.
background
The module derives the 32 crystallographic point groups and 7 crystal systems from periodic space-filling in three dimensions forced by the 8-tick octave. LatticeParams is the structure holding edge lengths $a,b,c$ and angles $alpha,beta,gamma$. CubicConstraint requires equal lengths together with right angles; orthorhombicConstraint requires only the right angles. Upstream, the module imports the general CrystalStructure definitions and the RS forcing chain that sets $D=3$.
proof idea
Term-mode proof. It introduces $p$ and pattern-matches the cubicConstraint hypothesis into its five conjuncts. The orthorhombicConstraint is then built by selecting the three angle conjuncts and discarding the two length equalities.
why it matters
The result encodes the hierarchy of crystal systems: cubic symmetry is strictly stronger than orthorhombic. It fills the step from the RS 8-tick geometry to the prediction of exactly seven crystal systems. The module doc-comment states that higher symmetry imposes more constraints, and this theorem supplies one concrete instance of that ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.