MagnetismTypesCert
plain-language theorem explainer
MagnetismTypesCert structures the assertion that the inductive type of magnetic orderings has cardinality exactly five, matching the canonical list diamagnetism through ferrimagnetism. Materials modelers working under Recognition Science dimensional assignments cite this to fix configDim at five for magnetic phases. The structure follows directly from the Fintype instance automatically derived on the five-constructor inductive type.
Claim. A structure certifying that the set of magnetic orderings has cardinality five: $ |M| = 5 $ where $ M = $ {diamagnetism, paramagnetism, ferromagnetism, antiferromagnetism, ferrimagnetism}.
background
Recognition Science assigns magnetic orderings to configDim = 5, enumerating the five standard cases as diamagnetism, paramagnetism, ferromagnetism, antiferromagnetism, and ferrimagnetism. The inductive type MagnetismType encodes precisely these constructors and derives Fintype, supplying the cardinality fact used in the certificate. The module provides the concrete classification layer that translates the abstract configDim parameter into material-specific orderings.
proof idea
The structure is introduced directly as a record whose single field records the Fintype.card equality. The equality holds by the automatic Fintype derivation on a finite inductive type with five explicit constructors; no lemmas or tactics are invoked.
why it matters
This supplies the fixed count of five magnetism types that the downstream definition magnetismTypesCert instantiates. It anchors the configDim = 5 assignment for magnetic phenomena inside the Recognition framework, consistent with the dimensional forcing steps that classify material responses. No open scaffolding questions attach at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.