magnetismType_count
plain-language theorem explainer
The set of magnetic ordering types has cardinality five, enumerating the canonical behaviors tied to configDim equal to five. Materials physicists cite this when classifying responses under the Recognition Science materials layer. The proof is a direct decision procedure on the Fintype instance derived from the inductive definition.
Claim. The set consisting of diamagnetism, paramagnetism, ferromagnetism, antiferromagnetism, and ferrimagnetism has cardinality five: $|M| = 5$ where $M$ denotes the type of magnetism orderings.
background
MagnetismType is the inductive type whose five constructors are diamagnetism, paramagnetism, ferromagnetism, antiferromagnetism, and ferrimagnetism; it derives DecidableEq, Repr, BEq, and Fintype. The module sets the five canonical magnetic orderings equal to configDim D = 5 in the B15 materials depth. The sole upstream result is the inductive definition of MagnetismType itself.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute Fintype.card directly from the derived Fintype instance on the inductive type.
why it matters
This supplies the five_types field inside the MagnetismTypesCert definition. It anchors the enumeration of magnetic behaviors at configDim = 5, extending the core Recognition Science framework (T8 fixes spatial D = 3) into the materials layer. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.