ceramicClassesCert
plain-language theorem explainer
The definition ceramicClassesCert constructs a concrete instance of the CeramicClassesCert structure by populating its cardinality field with the established count of five. Materials modelers working from configDim D = 5 would cite it to certify the five families of oxides, carbides, nitrides, borides, and silicates. The construction is a direct one-line field assignment drawn from the decide-based cardinality theorem.
Claim. Let CeramicClassesCert be the structure whose sole field requires that the finite cardinality of the type of ceramic classes equals 5. The definition sets this field to the theorem establishing that cardinality.
background
The module fixes configDim at D = 5 to produce exactly five canonical ceramic families. The type CeramicClass enumerates these families, and the upstream theorem ceramicClass_count proves its Fintype.card equals 5 by direct decision. The structure CeramicClassesCert packages this single cardinality assertion as a reusable certificate. Module documentation states: Five canonical ceramic families (= configDim D = 5): oxides, carbides, nitrides, borides, silicates.
proof idea
The definition is a one-line wrapper that instantiates CeramicClassesCert by assigning the value of the theorem ceramicClass_count to its five_classes field.
why it matters
This definition supplies the certified count of five classes required by the materials classification layer at configDim D = 5. It supports the Recognition Science program of deriving material families from the single functional equation and the T0-T8 forcing chain. No downstream theorems yet consume the certificate, leaving open its later use in property or stability derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.