MaterialsScienceCert
plain-language theorem explainer
MaterialsScienceCert records that the set of material classes has cardinality 5 and that the Oh group order equals 48. A condensed-matter theorist would cite it when mapping Recognition Science symmetry counts onto observed crystal systems. The structure is assembled directly from the inductive enumeration of the five classes and the explicit definition of ohGroupOrder.
Claim. A certificate consisting of the two assertions that the finite type of material classes (metals, ceramics, polymers, composites, semiconductors) has cardinality 5 and that the Oh group order equals $6 times 2^3$.
background
The module Materials Science from RS identifies five canonical material classes with the configuration dimension equal to 5. Crystal symmetry groups map to Q₃ sublattices of size 8, matching 2^D for spatial dimension D=3. The Oh group supplies the canonical cubic symmetry with order 48, written as 6 times 8 or 6 times 2^D.
proof idea
This is a structure definition with an empty proof body. It records the two field equalities by direct reference to the sibling inductive MaterialClass and the definition ohGroupOrder.
why it matters
The structure supplies the two invariants consumed by the downstream construction materialsScienceCert. It closes the materials-classification step that links the five classes to configDim D=5 and the group order to the eight-tick octave (T7) together with D=3 (T8). The module records zero sorry and zero axiom for this mapping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.