monopoleChargeQuantized
plain-language theorem explainer
The theorem confirms that the monopole charge function returns a natural number for every input sector n. Physicists citing the RS phi-lattice model for Dirac monopoles would use this to anchor the integer spectrum. The proof is a one-line term that supplies the witness n and closes by reflexivity.
Claim. For every natural number $n$, there exists a natural number $k$ such that the monopole charge in sector $n$ equals $k$.
background
The module treats the Dirac quantization condition $g_m e = n hbar c / 2$ inside the Recognition Science phi-lattice. The function monopoleCharge maps each natural number $n$ to itself, encoding the five charge sectors that match configDim $D=5$. Foundational arithmetic enters via the canonical Peano object from ArithmeticOf, which supplies the initial logicNatPeano structure used to interpret the sectors.
proof idea
The proof is a term-mode construction. It forms the existential witness by pairing the input $n$ with the reflexivity tactic on the defining equation of monopoleCharge.
why it matters
This result populates the quantized field inside magneticMonopoleCert, which assembles the full monopole certificate. It directly implements the module's claim that the magnetic charge spectrum is quantized in multiples of the Dirac unit on the phi-ladder, consistent with the five-sector prediction and the RS-native constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.