magneticPhenomenonCount
plain-language theorem explainer
The theorem establishes that Recognition Science yields exactly five magnetic phenomena from recognition charge currents. Model builders classifying ferromagnetism through diamagnetism would cite the cardinality result. The proof applies a decision procedure directly to the finite type structure of the inductive enumeration.
Claim. $ | { ferromagnetism, antiferromagnetism, ferrimagnetism, paramagnetism, diamagnetism } | = 5 $
background
The module Magnetism from RS treats magnetic phenomena as recognition charge currents, where the field B equals the current density relative to baseline. The inductive definition MagneticPhenomenon lists the five cases that realize this structure. This count matches the module's assertion of five phenomena corresponding to configDim D = 5, separating the zero-field case J = 0 from the applied-field case J > 0.
proof idea
The proof is a one-line wrapper invoking the decide tactic on the Fintype instance automatically derived from the inductive type MagneticPhenomenon.
why it matters
This supplies the five_phenomena component of the MagnetismCert structure that certifies the RS magnetism foundation. It realizes the module's claim of five canonical phenomena without invoking the forcing chain or phi-ladder. The result anchors the discrete enumeration in the A1 SM foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.