EMPhenomenon
plain-language theorem explainer
EMPhenomenon enumerates the five canonical electromagnetic phenomena in the Recognition Science derivation of Maxwell theory. Researchers deriving the four Maxwell equations from recognition cost and U(1) gauge structure on the Hilbert space would cite this type when counting distinct EM regimes. The definition is a direct inductive type with five constructors that automatically derives decidable equality and finite cardinality.
Claim. The inductive type whose constructors are the static electric field, static magnetic field, induction, radiation, and plasma regimes.
background
The module derives Maxwell's four equations (Gauss E, Gauss B, Faraday, Ampere-Maxwell) as U(1) gauge theory on the recognition Hilbert space, with the field identified as the J-cost of E·B normalized at the critical threshold. In three spatial dimensions the equation count equals 2^(D-1) = 4. The five phenomena are stated to match configDim D = 5. The imported Cost module supplies the J-cost functional used to define the EM field.
proof idea
This is an inductive definition that introduces five named constructors and derives DecidableEq, Repr, BEq, and Fintype in one declaration.
why it matters
The type supplies the five_phenomena field of MaxwellCert and the target of emPhenomenonCount, which proves Fintype.card EMPhenomenon = 5 by decide. It thereby completes the RS classification that links the four Maxwell equations (from 2^(D-1) with D=3) to exactly five observable EM regimes, closing the A1 SM-depth step in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.