monopoleCharge
plain-language theorem explainer
The declaration defines the monopole charge for sector n as the value n itself. Physicists deriving magnetic monopoles from the phi-lattice in Recognition Science cite it to encode the Dirac quantization condition. The definition is a direct identity that supplies the base case for the existence theorem and the five-sector cardinality result.
Claim. The magnetic monopole charge in sector $n$ is defined as $g_m(n) = n$ (in units where the fundamental Dirac charge is 1).
background
The module formalizes the Dirac quantization condition $g_m e = n hbar c / 2$, with the minimal monopole at $n=1$. In RS terms the charge lies on rung 1 of the phi-ladder relative to the Dirac string tension, and the spectrum is quantized in multiples of $g_D = hbar c / (2e)$. Five sectors are identified with configDim $D=5$.
proof idea
The declaration is a direct definition that equates monopoleCharge n to n by identity.
why it matters
It supplies the charge values required by MagneticMonopoleCert (whose quantized field asserts existence for every n and whose five_sectors field requires cardinality 5) and by the theorem monopoleChargeQuantized. The definition implements the Dirac quantization step stated in the module documentation and connects to the phi-ladder structure of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.