emPhenomenonCount
plain-language theorem explainer
The declaration establishes that the inductive type enumerating canonical electromagnetic phenomena in Recognition Science has cardinality exactly five. A physicist deriving Maxwell's equations from the recognition functional equation would cite this to confirm the configuration dimension matches D=5. The proof is a one-line decision procedure that computes the cardinality from the derived Fintype instance on the five-constructor inductive type.
Claim. The finite set of electromagnetic phenomena has cardinality $5$, consisting of static electric fields, static magnetic fields, induction, radiation, and plasma.
background
In the Maxwell Equations from RS module, electromagnetic phenomena are formalized via an inductive type whose five constructors are staticE, staticB, induction, radiation, and plasma; this type derives DecidableEq, Repr, BEq, and Fintype. The module treats EM as U(1) gauge theory on the recognition Hilbert space, with the field given by the J-cost at canonical thresholds, and states that five phenomena equal configDim D while four Maxwell equations equal 2^(D-1) for D=3. The upstream inductive definition supplies the Fintype instance required for cardinality computation.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds directly because the inductive type derives a Fintype instance whose cardinality is computed as five without further lemmas.
why it matters
This supplies the five_phenomena component of the MaxwellCert definition that certifies the full set of Maxwell equations derived from Recognition Science. It instantiates the framework landmark that D=3 spatial dimensions force 2^(D-1)=4 equations and configDim D=5 phenomena. No open scaffolding questions are closed by this result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.