monopoleChargeSectorsCard
plain-language theorem explainer
The magnetic monopole charge spectrum in the Recognition Science phi-lattice model consists of exactly five sectors labeled by the integers 1 through 5. Physicists checking the Dirac quantization condition g_m e = n hbar c / 2 would cite this result to confirm the discrete spectrum on the phi-ladder. The proof is a direct computation of the cardinality of the finite set {1,2,3,4,5}.
Claim. Let $S$ be the set of monopole charge sectors. Then $|S| = 5$.
background
In the Recognition Science framework the Dirac quantization condition reads $g_m e = n hbar c / 2$, with the smallest monopole at $n=1$. The phi-lattice places these charges on rungs of the phi-ladder relative to the Dirac string tension, and the module states that five sectors ($n=1,2,3,4,5$) equal the configuration dimension $D=5$. The upstream definition supplies the concrete set $S = {1,2,3,4,5}$.
proof idea
One-line wrapper that applies the decide tactic to evaluate the cardinality of the finite set of sectors.
why it matters
This result supplies the five_sectors field inside the MagneticMonopoleCert definition, which certifies the quantized spectrum. It realizes the RS prediction that magnetic charge is quantized in multiples of $g_D = hbar c / (2e)$ on the phi-ladder and aligns with the eight-tick octave structure. It touches the open question of how the sector count $D=5$ reconciles with the spatial dimension $D=3$ derived in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.