maxwell_eq_2pwr
plain-language theorem explainer
The theorem equates the number of Maxwell equations to 2 raised to (D minus 1) for three spatial dimensions. Researchers deriving classical electromagnetism from recognition principles would reference this identity. The proof relies on a direct computational check that confirms the numerical match without further reasoning.
Claim. The number of Maxwell equations equals $2^{D-1}$ when the spatial dimension $D$ is 3.
background
Recognition Science treats Maxwell's equations as arising from U(1) gauge theory on the recognition Hilbert space, with exactly four equations corresponding to the formula 2^(D-1). The module sets the Maxwell equation count to 4 and defines 2^(3-1) to match this count for D equal to 3. Upstream definitions establish these values explicitly as constants in natural numbers. This local setting confirms the alignment of the four standard equations (Gauss E, Gauss B, Faraday, Ampere-Maxwell) with the general dimensional pattern in the framework.
proof idea
The proof applies the decide tactic directly to the equality of the two natural number definitions, confirming the identity by computation.
why it matters
This declaration fills the basic count verification step in the Maxwell equations derivation from RS, linking to the framework's T8 where D equals 3 spatial dimensions. It supports the module's claim that EM equals 2^(D-1) equations and feeds into broader consistency checks for the five canonical EM phenomena. The result closes a numerical consistency point without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.