orthogonalSystem_count
plain-language theorem explainer
The declaration proves there are exactly five orthogonal crystal systems among the seven that partition three-dimensional lattices. Crystallographers and condensed-matter theorists would cite the count when separating orthogonal-axis systems from the two oblique ones. The proof is a one-line decision procedure that evaluates the cardinality of the finite inductive type whose five constructors are cubic, tetragonal, orthorhombic, trigonal, and hexagonal.
Claim. The set of orthogonal crystal systems has cardinality $5$.
background
The module CrystalSystemsFromConfigDim partitions the seven crystal systems of three-dimensional crystallography according to axis orthogonality. OrthogonalCrystalSystem is the inductive type whose constructors are precisely the five systems whose axes are mutually perpendicular: cubic, tetragonal, orthorhombic, trigonal, and hexagonal. The module documentation records that these five arise when the configuration dimension equals five, leaving monoclinic and triclinic as the oblique pair.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic computes Fintype.card directly from the automatically derived Fintype instance on the inductive type OrthogonalCrystalSystem.
why it matters
The result supplies the field five_orthogonal inside the certificate crystalSystemsCert, which also records the total of seven systems and the Bravais count of fourteen. It therefore closes the enumeration step that links the Recognition framework's D = 3 spatial dimensions to the standard crystallographic partition without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.