Pith. sign in
module module moderate

IndisputableMonolith.Physics.MagneticMonopoleFromPhiLattice

show as:
view Lean formalization →

The module derives Dirac quantization for magnetic monopole charge from the phi-lattice in Recognition Science. Physicists studying monopole spectra or lattice-based unification would cite the charge-sector definitions and quantization result. The structure introduces monopoleCharge and proves monopoleChargeQuantized via lattice periodicity and sector cardinality.

claimIn the $\phi$-lattice the monopole charge $q_m$ takes discrete values $q_m = n \cdot q_0$ for integer $n$, satisfying the Dirac condition $e g_m / \hbar c \in \mathbb{Z}$.

background

The module sits in the Physics domain and imports Mathlib. It builds on the J-cost function and phi-ladder from the forcing chain (T5-T8). Key objects are monopoleCharge (the charge extracted from lattice defects), monopoleChargeQuantized (the quantization theorem), and MagneticMonopoleCert (the certificate object). The setting assumes the eight-tick octave and D=3 from upstream.

proof idea

This is a definition module, no proofs. Definitions introduce charge sectors; theorems establish quantization by counting sectors and applying lattice periodicity.

why it matters in Recognition Science

The module supplies the quantized monopole charge required for any Recognition Science account of electromagnetism. It feeds parent results on particle spectra and unification steps that rely on the phi-lattice in three dimensions.

scope and limits

declarations in this module (6)