crystalSystemsCert
plain-language theorem explainer
The crystalSystemsCert definition packages the standard enumeration of three-dimensional crystal systems into a single certificate. Researchers in solid-state physics or crystallography would cite it when confirming that five of the seven systems admit orthogonal axes while the remaining two are oblique, producing fourteen Bravais lattices in total. The construction is a direct structure literal that substitutes the results of three decision-based lemmas for the three required fields.
Claim. Let CrystalSystemsCert be the structure whose fields assert that the cardinality of OrthogonalCrystalSystem equals 5, that the total number of crystal systems satisfies $7=5+2$, and that the Bravais lattice count equals 14. Then crystalSystemsCert is the element of this structure obtained by substituting the known values of these three counts.
background
Recognition Science places three-dimensional crystallography inside the configDim framework, where five orthogonal-axis systems arise when the configuration dimension is five. The module enumerates the seven crystal systems as cubic, tetragonal, orthorhombic, trigonal, and hexagonal (orthogonal) together with monoclinic and triclinic (oblique). Fourteen Bravais lattices then follow by allowing primitive and centered variants for each system.
proof idea
The definition is a structure instance that directly assigns the three fields of CrystalSystemsCert to the corresponding upstream theorems. orthogonalSystem_count supplies the orthogonal cardinality, seven_systems_partition supplies the total count identity, and bravais_eq supplies the Bravais lattice count. No further reasoning is required beyond these substitutions.
why it matters
This certificate closes the crystallography section of the Physics module by recording the standard seven-system partition that follows from three spatial dimensions. It supplies a reusable witness for any later argument that invokes the number of crystal systems or Bravais lattices. The construction aligns with the framework's derivation of D equals three and the resulting discrete lattice structures, though no direct link to the phi-ladder or J-cost appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.