maxwellCert
plain-language theorem explainer
maxwellCert constructs a certificate asserting that the recognition framework produces exactly four Maxwell equations and five canonical electromagnetic phenomena. A physicist deriving gauge theories from the J-cost functional would cite it to confirm the EM sector matches standard Maxwell theory in three dimensions. The definition is a direct record construction that references the equation count equality and a decidable count of phenomena.
Claim. The Maxwell certificate is the structure asserting that the number of Maxwell equations equals 4, that this number equals $2^2$, and that the cardinality of the set of electromagnetic phenomena equals 5, where the equation count follows from $2^{D-1}$ for spatial dimension $D=3$ and the phenomena count equals the configuration dimension.
background
In the Recognition Science framework the electromagnetic sector is realized as a U(1) gauge theory on the recognition Hilbert space, with the field given by the J-cost at the canonical threshold. MaxwellCert packages three properties required for certification: the equation count equals four, this count equals two to the power of two, and there are five electromagnetic phenomena. These properties follow from the general counting rule that the number of equations is $2^{D-1}$ and the number of phenomena equals the configuration dimension $D=5$.
proof idea
The definition builds the MaxwellCert record by assigning the four-equation field to the upstream theorem that the count equals 4, the square-equality field to a decide tactic, and the phenomena field to the upstream theorem that the cardinality of EMPhenomenon equals 5. It is a direct record literal that relies on reflexivity for the base count and decidability for the remaining two fields.
why it matters
This definition certifies the electromagnetic sector inside the Recognition Science derivation, linking the four equations to the eight-tick octave and $D=3$ via the $2^{D-1}$ counting rule. It supports the claim that Maxwell theory emerges from the forcing chain and the recognition composition law without additional postulates. No downstream theorems depend on it yet, but it closes the classical EM certification step in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.