MaxwellCert
plain-language theorem explainer
MaxwellCert records that the Maxwell equation count equals 4 and also equals 2 squared, while the inductive type of electromagnetic phenomena has cardinality 5. A physicist reconstructing classical electromagnetism from the recognition functional equation would cite the structure to confirm agreement with the D=3 prediction. The definition assembles these facts directly from the constant maxwellCount and the Fintype instance on the five-constructor inductive type.
Claim. The structure asserts that the number of Maxwell equations equals 4, that this number equals $2^2$, and that the set of canonical electromagnetic phenomena has cardinality 5.
background
In the Recognition Science framework, electromagnetism is realized as a U(1) gauge theory on the recognition Hilbert space, with the field strength obtained by evaluating the J-cost at the canonical threshold. The module states that Maxwell's four equations (Gauss E, Gauss B, Faraday, Ampere-Maxwell) equal $2^{D-1}$ for $D=3$ spatial dimensions. Five canonical phenomena (static E, static B, induction, radiation, plasma) are enumerated by an inductive type whose cardinality matches the configuration dimension $D=5$ and equals the constant 4 supplied by the upstream definition maxwellCount.
proof idea
MaxwellCert is a structure definition that directly packages the three equalities. The first two fields reference the constant maxwellCount set to 4 and its equality to 2 squared. The third field invokes the Fintype.card instance derived from the five constructors of the inductive type of electromagnetic phenomena.
why it matters
The structure certifies that the recognition-derived electromagnetism reproduces the classical equation count $2^{D-1}$ and the five-phenomena enumeration required by the framework for $D=3$. It is instantiated by the downstream maxwellCert definition to produce an explicit witness. The construction closes the A1 SM Depth section by confirming consistency with the eight-tick octave and the Recognition Composition Law applied to the U(1) gauge field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.