CeramicClass
plain-language theorem explainer
The declaration introduces an inductive type with five cases that enumerate the canonical ceramic families tied to configDim equal to 5. A materials physicist would cite the enumeration when partitioning ceramics according to the five-dimensional configuration model. The construction is a direct inductive definition that derives finite type cardinality and equality decidability automatically.
Claim. The set of ceramic classes consists of the five families oxides, carbides, nitrides, borides, and silicates, each corresponding to one element in the configDim $D=5$ classification.
background
The module Ceramic Classes from configDim establishes the materials depth by fixing configDim to 5 and identifying the five families: oxides, carbides, nitrides, borides, silicates. This choice aligns with the Recognition Science assignment of five canonical classes to that dimension. No prior lemmas are required; the definition stands alone with zero axioms or sorrys.
proof idea
The declaration is the inductive definition itself, introducing the five constructors and automatically deriving DecidableEq, Repr, BEq, and Fintype instances.
why it matters
The definition is used by the theorem that certifies the cardinality equals 5 and by the structure that packages that fact as a certificate. It completes the materials classification step for configDim = 5 in the framework, where D = 5 selects these five families. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.