numCrystalSystems
plain-language theorem explainer
The declaration asserts that the number of crystal systems is seven. Crystallographers and solid-state physicists cite this count when classifying the 32 point groups into symmetry classes that permit periodic filling of three-dimensional space. The definition is a direct constant assignment that records the outcome of the space-filling analysis derived from the eight-tick structure.
Claim. The number of crystal systems is $7$.
background
In Recognition Science, three-dimensional space arises from the eight-tick octave (T7) that forces D = 3 spatial dimensions (T8). Periodic arrangements of identical units must respect the underlying ledger geometry, which restricts rotational symmetries to orders 1, 2, 3, 4, and 6 because five-fold and higher orders cannot tile 3D space without gaps. The module documentation states that the 32 crystallographic point groups cluster into seven systems according to their essential symmetry elements: triclinic (no essential symmetry), monoclinic (one 2-fold axis or mirror), orthorhombic (three perpendicular 2-fold axes), tetragonal (one 4-fold axis), trigonal (one 3-fold axis), hexagonal (one 6-fold axis), and cubic (four 3-fold axes). Upstream structures from PhiForcingDerived and LedgerFactorization calibrate the J-cost and ledger factorization that ground these geometric constraints.
proof idea
The definition is a direct constant assignment of the natural number 7 with no lemmas applied and no tactics used.
why it matters
This definition supplies the integer that the downstream theorem crystal_systems_count equates to the length of allCrystalSystems. It realizes the module prediction that exactly seven crystal systems arise from the 3D space-filling constraint. The count connects to the Recognition Science chain in which T7 and T8 fix the allowed symmetries and the crystallographic restriction follows from the ledger geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.