cubicConstraint
plain-language theorem explainer
Cubic lattice parameters satisfy a = b = c with all angles exactly 90 degrees. Materials scientists classifying Bravais lattices cite this definition when applying the seven-system taxonomy derived from space-filling rules. It is implemented as a direct propositional definition of the geometric conditions on the parameter record.
Claim. A lattice with parameters $a, b, c, α, β, γ$ satisfies the cubic constraint precisely when $a = b = c$ and $α = β = γ = 90^∘$.
background
LatticeParams is the record holding three 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 derives the seven crystal systems from the 8-tick octave that forces three spatial dimensions and the consequent space-filling restrictions that permit only rotation orders 1, 2, 3, 4, 6. Cubic symmetry is the highest-symmetry case, defined by four threefold axes along the body diagonals.
proof idea
This is a definition that directly states the conjunction of equalities on the lattice parameters.
why it matters
The definition is invoked by the theorem cubic_most_constrained to establish that cubic symmetry implies the orthorhombic constraints. It supplies the concrete geometric predicate for the cubic entry in the enumeration of exactly seven crystal systems that the module obtains from the Recognition Science 8-tick structure and D = 3. The module doc states that this clustering yields the observed 32 point groups and 14 Bravais lattices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.