ceramicClass_count
plain-language theorem explainer
The set of canonical ceramic families in the Recognition Science materials model has cardinality five. Materials researchers enumerating families at configDim = 5 cite this result to fix the count of oxide, carbide, nitride, boride, and silicate classes. The proof is a one-line decision procedure that exhausts the inductive constructors.
Claim. The set of canonical ceramic families has cardinality five: $5$.
background
CeramicClass is formalized as an inductive type whose five constructors are oxide, carbide, nitride, boride, and silicate; the type derives a Fintype instance so that cardinality is computable by enumeration. The module sets configDim to D = 5 and identifies these five families as the canonical ceramic classes under that dimension. The sole upstream dependency is the inductive definition of CeramicClass itself.
proof idea
The proof applies the decide tactic, which automatically verifies the Fintype.card equality by exhaustive enumeration of the five constructors.
why it matters
The theorem supplies the five_classes field inside the CeramicClassesCert definition, anchoring the materials classification at configDim = 5. It closes the enumeration step for the five families without introducing new hypotheses or open questions in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.