bravaisLatticeCount
plain-language theorem explainer
bravaisLatticeCount defines the total number of Bravais lattices in three dimensions as the constant 14. Crystallographers and condensed-matter physicists cite this value when partitioning the seven crystal systems into their lattice realizations. The declaration is introduced as a direct numerical assignment with no computation or auxiliary lemmas.
Claim. The number of distinct Bravais lattices in three-dimensional space equals $14$.
background
The module Crystal Systems from configDim treats seven crystal systems as the basic partition of 3D crystallography. Five systems rest on orthogonal axes (configDim D = 5): cubic, tetragonal, orthorhombic, trigonal, and hexagonal. The remaining two, monoclinic and triclinic, are oblique. The relation 14 Bravais lattices = 7 systems × 2 (primitive plus one centering) supplies the numerical constant recorded here.
proof idea
The declaration is a direct definition that assigns the natural number 14 to the Bravais lattice count.
why it matters
This constant anchors the certification of crystal systems inside the Recognition framework. It is referenced by the equality theorem bravais_eq and by the structure CrystalSystemsCert, which records five orthogonal systems plus two oblique ones. The value aligns with the framework landmark T8 that forces D = 3 spatial dimensions and supports the link between the phi-ladder and physical lattice structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.