point_groups_sum
plain-language theorem explainer
The theorem verifies that the seven crystal systems together contain exactly 32 crystallographic point groups. A crystallographer or solid-state physicist working in Recognition Science would cite it to confirm the enumeration matches the standard count derived from space-filling constraints. The proof is a one-line term that applies native_decide to evaluate the finite list sum directly.
Claim. The sum, over the seven crystal systems, of the number of point groups belonging to each system equals 32.
background
Crystal symmetry emerges in Recognition Science from the 8-tick octave that forces three spatial dimensions. Periodic filling of this space restricts rotations to orders 1, 2, 3, 4, and 6, yielding exactly 32 point groups that cluster into seven crystal systems (triclinic through cubic) as stated in the module derivation CM-003.
proof idea
The proof is a term-mode application of native_decide. It evaluates the list allCrystalSystems, maps each system to its point-group count via numPointGroups, sums the resulting numbers, and confirms equality with the constant totalPointGroups.
why it matters
This result closes the point-group enumeration step in the crystal-symmetry derivation. It confirms the module prediction of 32 groups arising from the 8-tick forced 3D geometry and space-filling rules, supporting later counts of 14 Bravais lattices and 230 space groups. The upstream forcing structure supplies the dimensional and symmetry constraints that make the finite list exhaustive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.