MagneticMonopoleCert
plain-language theorem explainer
MagneticMonopoleCert packages the assertions that monopole charges map natural numbers to natural numbers and that exactly five sectors exist in the phi-lattice model. A physicist working on Dirac quantization or RS extensions of the standard model would cite this structure to confirm the discrete spectrum. The declaration is a plain structure definition that directly bundles the upstream monopoleCharge identity and the five-element Finset with no reduction or tactic steps.
Claim. A certificate structure requiring that the monopole charge function satisfies $g_m(n) = k$ for some natural number $k$, for every natural number $n$, and that the finite set of monopole charge sectors has cardinality exactly 5.
background
The module develops the magnetic monopole from the phi-lattice, starting from the Dirac quantization condition $g_m e = n hbar c / 2$. The monopoleCharge definition implements quantization by returning the input natural number directly. The monopoleChargeSectors definition assembles the set {1, 2, 3, 4, 5} as the five canonical sectors. This local setting places the smallest monopole on rung 1 of the phi-ladder relative to the Dirac string tension, with the spectrum quantized in multiples of $g_D = hbar c / (2e)$. The structure MagneticMonopoleCert collects these two properties into a single certificate object. Upstream results supply the doc-comments 'Dirac quantization: monopole charge is quantized' for monopoleCharge and 'Five canonical monopole charge sectors' for monopoleChargeSectors.
proof idea
As a structure definition with an empty proof body, it simply declares the two fields by direct reference to the monopoleCharge and monopoleChargeSectors definitions already present in the same module.
why it matters
The structure supplies the type instantiated by the downstream magneticMonopoleCert definition, which supplies concrete values for the quantized and five_sectors fields. It encodes the RS prediction that the magnetic charge spectrum is quantized on the phi-ladder. This touches the framework landmark of five sectors corresponding to configDim D = 5, separate from the spatial dimension D = 3 in the main forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.