bravais_lattices_sum
plain-language theorem explainer
The theorem states that summing the Bravais lattice counts over the seven crystal systems equals exactly 14. Crystallographers and condensed-matter physicists cite it to confirm the standard lattice enumeration. The proof is a one-line native_decide that evaluates the explicit list map and constant directly from the definitions.
Claim. Let $S$ range over the seven crystal systems. Let $n_B(S)$ be the number of Bravais lattices for system $S$. Then $n_B(S_1) + n_B(S_2) + n_B(S_3) + n_B(S_4) + n_B(S_5) + n_B(S_6) + n_B(S_7) = 14$.
background
The CrystalSymmetry module derives crystal symmetry from the 8-tick structure that forces three spatial dimensions and the space-filling constraint that restricts rotations to orders 1, 2, 3, 4, 6. allCrystalSystems is the list [triclinic, monoclinic, orthorhombic, tetragonal, trigonal, hexagonal, cubic]. numBravaisLattices maps each system to its allowed centering types (P, C, I, F, R), yielding the values 1, 2, 4, 2, 1, 1, 4. totalBravaisLattices is the constant 14.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the sum of the mapped list and compare it to the constant totalBravaisLattices.
why it matters
This theorem completes the Bravais lattice count inside the Recognition Science crystal symmetry derivation (CM-003). It confirms the module prediction of exactly 14 Bravais lattices that follows from the 8-tick octave forcing D = 3 and the crystallographic restriction. The module documentation lists the result among the core predictions: exactly 14 Bravais lattices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.