totalBravaisLattices
plain-language theorem explainer
The total number of Bravais lattices in three dimensions is fixed at fourteen. Recognition Science derivations of crystal symmetry cite this count to confirm that seven crystal systems plus allowed centerings exhaust all periodic space-filling arrangements. The definition supplies a constant that a downstream summation applies directly to close the enumeration.
Claim. The total number of Bravais lattices is $14$.
background
The module derives crystal symmetry from the eight-tick octave that forces three spatial dimensions. Periodic arrangements of identical units must fill space without gaps or overlaps, which restricts rotational symmetries to orders 1, 2, 3, 4, and 6. The seven crystal systems arise by grouping the 32 point groups according to their essential symmetry elements: triclinic with no essential symmetry, monoclinic with one twofold axis or mirror, orthorhombic with three perpendicular twofold axes, tetragonal with one fourfold axis, trigonal with one threefold axis, hexagonal with one sixfold axis, and cubic with four threefold axes along body diagonals.
proof idea
The definition is a direct constant assignment of the integer fourteen.
why it matters
This definition supplies the target value for the summation theorem that verifies the total across all crystal systems. It realizes the module prediction that exactly fourteen Bravais lattices arise once the space-filling constraints from three-dimensional geometry are imposed. The result supports the further claim that two hundred thirty space groups exist when translations are included.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.