CeramicClassesCert
plain-language theorem explainer
The certificate structure for ceramic classes requires that the finite cardinality of the ceramic class type equals five. Materials researchers in the Recognition Science framework cite it to confirm the five families of oxides, carbides, nitrides, borides, and silicates. The definition consists of a single field in a structure declaration with no further proof.
Claim. A structure is defined by the field asserting that the finite type cardinality of the set of ceramic classes equals five, where the ceramic classes are the five families given by the inductive type with constructors oxide, carbide, nitride, boride, and silicate.
background
The module establishes five canonical ceramic families corresponding to configuration dimension D = 5: oxides, carbides, nitrides, borides, and silicates. The inductive definition of the ceramic class type enumerates these five cases and derives instances for decidable equality, representation, boolean equality, and finite type. This provides the local setting for materials classification in Recognition Science, where configDim fixes the number of classes at five.
proof idea
The declaration is a structure definition. It directly specifies the single field as the equality between the finite type cardinality of the ceramic class type and five. No tactics or lemmas are invoked; the body is empty.
why it matters
This supplies the type for the downstream definition that constructs an explicit witness using the count from the inductive type. It anchors the materials section by equating the five families to configDim D = 5, aligning with the framework's derivation of discrete classes from the J-function and phi-ladder. No open questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.