OrthogonalCrystalSystem
OrthogonalCrystalSystem enumerates the five crystal systems with mutually orthogonal axes in three-dimensional space as an inductive type. Recognition Science modelers and crystallographers cite it when partitioning the seven crystal systems into orthogonal and oblique classes to reach the Bravais lattice count. The definition is a direct inductive enumeration that automatically derives Fintype, DecidableEq, Repr, and BEq instances.
claimLet $O$ be the inductive type with constructors cubic, tetragonal, orthorhombic, trigonal, and hexagonal.
background
In the Recognition Science framework the spatial dimension is fixed at D=3 by the eight-tick octave of the forcing chain. The module isolates the five orthogonal-axis systems (cubic, tetragonal, orthorhombic, trigonal, hexagonal) that correspond to configDim D=5, leaving monoclinic and triclinic as the two oblique systems. This partition is the prerequisite for expressing the fourteen Bravais lattices as seven systems each admitting a primitive and a centered realization.
proof idea
The declaration is a direct inductive definition that introduces the five constructors and derives the Fintype, DecidableEq, Repr, and BEq instances via the deriving clause.
why it matters in Recognition Science
The definition supplies the type whose cardinality is asserted equal to five inside CrystalSystemsCert, which simultaneously records the seven-system total and the fourteen Bravais lattices. It therefore implements the orthogonal restriction required by configDim D=5 inside the D=3 spatial setting fixed by T8. No open scaffolding remains; the enumeration is closed and used directly by the certification structure.
scope and limits
- Does not enumerate the oblique systems monoclinic and triclinic.
- Does not incorporate lattice centering or Bravais variants.
- Does not define metric parameters or symmetry groups for each system.
- Does not link to the phi-ladder or mass formulas.
formal statement (Lean)
20inductive OrthogonalCrystalSystem where
21 | cubic
22 | tetragonal
23 | orthorhombic
24 | trigonal
25 | hexagonal
26 deriving DecidableEq, Repr, BEq, Fintype
27