CrystalSystemsCert
plain-language theorem explainer
CrystalSystemsCert packages the standard counts for 3D crystal systems and Bravais lattices into one structure for use in Recognition derivations. Physicists checking lattice symmetry consistency with configDim would reference it when confirming the orthogonal-axis partition. The definition is a direct bundling of three numerical facts taken from the inductive enumeration of five orthogonal systems and the constant Bravais count.
Claim. Let $O$ be the set of orthogonal crystal systems (cubic, tetragonal, orthorhombic, trigonal, hexagonal). The structure asserts $|O|=5$, that the total number of crystal systems is $7=5+2$, and that the number of Bravais lattices equals 14.
background
The module derives crystal systems from configDim in the Recognition Science setting, where seven systems partition 3D lattices. Five systems have orthogonal axes (cubic through hexagonal) as listed by the inductive type OrthogonalCrystalSystem; the remaining two (monoclinic, triclinic) are oblique. The constant bravaisLatticeCount is defined directly as 14, matching the standard 7 systems each admitting primitive and centered variants. This local convention ties the orthogonal count of 5 to configDim D=5 and the overall spatial dimension D=3.
proof idea
As a structure definition, CrystalSystemsCert simply declares three fields that hold the required numerical equalities. It draws the cardinality 5 from the inductive enumeration of OrthogonalCrystalSystem and the value 14 from the constant definition bravaisLatticeCount. No tactics or lemmas beyond these two sibling definitions are applied.
why it matters
The structure feeds the downstream instantiation crystalSystemsCert, which populates the fields via orthogonalSystem_count and seven_systems_partition. It supplies the standard 3D crystallography partition required by the Recognition framework, aligning with T8 (D=3) and the configDim-derived orthogonal count. No open questions are closed here, but the declaration completes the enumeration step for lattice symmetries before further forcing-chain applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.