MagneticPhenomenon
plain-language theorem explainer
MagneticPhenomenon enumerates the five canonical magnetic phenomena as constructors in the Recognition Science treatment of magnetism as recognition charge currents. Workers deriving B from current density or certifying zero-field and applied-field J-cost properties cite this enumeration to fix the configuration dimension at 5. The declaration is a direct inductive definition that derives DecidableEq, Repr, BEq and Fintype instances with no further obligations.
Claim. The inductive type enumerating magnetic phenomena consists of the five constructors ferromagnetism, antiferromagnetism, ferrimagnetism, paramagnetism and diamagnetism. It carries decidable equality and is finite.
background
The MagnetismFromRS module identifies magnetic phenomena with recognition charge currents, writing the field B as recognition current density relative to baseline. Five canonical cases are stated to realize configuration dimension 5. At zero field the J-cost is zero; under applied field the J-cost is positive for any ratio r ≠ 1.
proof idea
The declaration is a direct inductive definition with five constructors. The deriving clause installs DecidableEq, Repr, BEq and Fintype instances automatically.
why it matters
The definition supplies the five-phenomena cardinality required by magneticPhenomenonCount and by the five_phenomena field of MagnetismCert. It realizes the module statement that five phenomena equal configDim D = 5. The enumeration precedes any derivation of magnetic properties from the forcing chain or recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.