bravais_eq
plain-language theorem explainer
The declaration equates the Bravais lattice count to 14. Crystallographers and solid-state physicists cite it when confirming the partition of three-dimensional crystals into seven systems with their associated lattice types. The proof is a one-line reflexivity that matches the explicit definition of the count directly to the integer 14.
Claim. The number of Bravais lattices in three dimensions equals 14.
background
The module on crystal systems from configuration dimension partitions three-dimensional space into seven crystal systems: five orthogonal-axis systems (cubic, tetragonal, orthorhombic, trigonal, hexagonal) and two oblique systems (monoclinic, triclinic). The Bravais lattice count is defined directly as the natural number 14, corresponding to each system admitting a primitive lattice plus one centering variant. The upstream definition sets this count explicitly to 14 with no further computation.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of the Bravais lattice count.
why it matters
This supplies the Bravais count to the crystal systems certificate, which records five orthogonal systems, seven total systems, and the 14 lattices. It aligns with the framework derivation of three spatial dimensions and the standard 7-by-2 crystallographic partition. The module records zero sorry or axiom in the formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.