MagnetismCert
plain-language theorem explainer
MagnetismCert bundles three conditions that certify magnetism as recognition currents in RS: exactly five canonical phenomena, vanishing J-cost at equilibrium ratio one, and strictly positive J-cost for any other positive ratio. A physicist deriving magnetic fields from recognition charge currents would cite this to anchor the five cases (ferromagnetism through diamagnetism) as configDim equals five. The declaration is a plain structure definition that packages the properties with no derivation steps.
Claim. A structure asserting that the set of magnetic phenomena has cardinality five, that the recognition cost function satisfies $J(1)=0$, and that $J(r)>0$ for every positive real $r$ different from one.
background
The module treats magnetic phenomena as recognition charge currents, with the magnetic field identified with recognition current density. MagneticPhenomenon is the inductive type whose five constructors are ferromagnetism, antiferromagnetism, ferrimagnetism, paramagnetism and diamagnetism; the Fintype instance on this type supplies the cardinality claim. Jcost is the cost function imported from the Cost module and satisfies the zero-field condition J=0 together with the applied-field condition J>0. The local setting states that these five phenomena correspond to configDim D=5 and that the structure records the equilibrium and deviation properties of the recognition current.
proof idea
The declaration is a structure definition with no proof body. It directly records the three fields: the cardinality equality obtained from the Fintype instance on MagneticPhenomenon, the equality Jcost 1 = 0, and the universal quantification over positive reals that encodes the applied-field positivity.
why it matters
MagnetismCert supplies the type that magnetismCert instantiates, thereby closing the Lean interface for the magnetism-from-RS foundation. It encodes the claim that five phenomena arise once recognition currents are admitted, consistent with the module statement that magnetic field equals recognition current density. The construction touches the Recognition Science counting of canonical cases but does not yet link to the eight-tick octave or the spatial-dimension forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.