maxwell_eq_4
plain-language theorem explainer
The declaration fixes the count of Maxwell equations derived from recognition costs at four. Workers on U(1) gauge theories in the Recognition Science setting cite this when confirming the structure matches 2^(D-1) for three spatial dimensions. The proof applies reflexivity directly to the definition of maxwellCount.
Claim. The Maxwell equation count in the Recognition Science derivation equals four: $4 = 4$.
background
The module derives Maxwell's equations from the recognition cost function J on the Hilbert space, identifying them with the U(1) gauge theory components. It lists the four equations as Gauss E, Gauss B, Faraday, and Ampere-Maxwell, noting that this number is 2^(D-1) with D=3 from the forcing chain. The upstream definition provides maxwellCount as the natural number 4, which serves as the fixed count for certification of electromagnetic phenomena.
proof idea
The proof consists of a single reflexivity step that matches the left-hand side to its definition as the constant four.
why it matters
This result populates the four_eqs component of the MaxwellCert definition, which certifies the complete electromagnetic structure including the five phenomena. It realizes the counting relation 4 = 2^(D-1) stated in the module for D=3, consistent with the T8 step in the forcing chain that sets three spatial dimensions. The declaration closes the enumeration needed for the EMPhenomenon count in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.