magnetismType_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the five types from the J-function or forcing chain.
- Does not address physical realizability or stability of each ordering.
- Does not compute transition temperatures or critical fields.
Lean usage
def magnetismTypesCert : MagnetismTypesCert where five_types := magnetismType_countformal statement (Lean)
24theorem magnetismType_count : Fintype.card MagnetismType = 5 := by decide
proof body
25