monopoleChargeSectors
plain-language theorem explainer
The definition enumerates the five canonical monopole charge sectors as the finite set of natural numbers {1,2,3,4,5}. Physicists checking the Dirac quantization spectrum in the Recognition Science phi-lattice model cite this set when confirming the n values in g_m e = n hbar c / 2. The construction is a direct finite-set literal with no computation or lemmas applied.
Claim. The monopole charge sectors are the finite set $S = {1,2,3,4,5} subset mathbb{N}$.
background
The module derives magnetic monopoles from the phi-lattice under the Dirac quantization condition g_m e = n hbar c / 2. In RS terms the magnetic charge g_m sits on rung 1 of the phi-ladder relative to the Dirac string tension, and the five sectors n=1 to 5 are identified with configDim D=5. The magnetic charge spectrum is therefore quantized in multiples of g_D = hbar c / (2e).
proof idea
The definition is a direct finite-set literal containing the first five positive integers.
why it matters
MagneticMonopoleCert uses the set to assert both quantization of the charge and that exactly five sectors exist; the downstream theorem monopoleChargeSectorsCard confirms its cardinality equals 5. The definition therefore supplies the concrete n values required by the Recognition Science prediction that the monopole spectrum is quantized on the phi-ladder, consistent with the eight-tick octave and D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.