MagnetismType
plain-language theorem explainer
The inductive definition enumerates the five canonical magnetic orderings assigned to configDim = 5 in Recognition Science materials theory. Researchers classifying magnetic responses or proving finite enumerations in the configDim framework cite this type when building cardinality results or certification structures. It is introduced directly as an inductive type whose derived Fintype and DecidableEq instances follow automatically from the five constructors.
Claim. The magnetic ordering type is the finite set consisting of diamagnetism, paramagnetism, ferromagnetism, antiferromagnetism, and ferrimagnetism.
background
The module treats configDim = 5 as the discrete classification dimension that isolates the five standard magnetic orderings. Each ordering corresponds to a distinct response to an external field: diamagnetism produces induced moments opposing the field, paramagnetism produces weak alignment, ferromagnetism produces spontaneous long-range order, antiferromagnetism produces alternating spin sublattices, and ferrimagnetism produces unequal opposing sublattice moments. The local convention therefore equates the cardinality of this type with the value of configDim for magnetism.
proof idea
The declaration is the inductive definition that introduces exactly five constructors, one per ordering. The derived instances for DecidableEq, Repr, BEq, and Fintype are generated automatically by the Lean inductive machinery; no explicit proof steps are required.
why it matters
The type supplies the domain for the downstream theorem magnetismType_count, which asserts Fintype.card MagnetismType = 5, and for the certification structure MagnetismTypesCert that packages the same equality. It therefore realizes the configDim = 5 assignment for magnetic materials inside the Recognition Science framework, where configDim governs the discrete taxonomy of material responses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.