landauPoleDescription
plain-language theorem explainer
This definition supplies a compact textual summary of the QED Landau pole under Recognition Science. A physicist studying UV cutoffs in unification scenarios would cite it when contrasting the divergent coupling with Planck-scale discreteness. The definition consists of a single string literal that embeds the physical statement without computation or lemmas.
Claim. In QED the electromagnetic coupling diverges at an energy scale of approximately $10^{286}$ GeV; Recognition Science supplies a natural cutoff via Planck-scale discreteness.
background
The module derives running couplings from φ-ladder scaling. Energy scales correspond to distinct rungs on the φ-ladder, with J-cost optimization varying across those rungs. Upstream, Energy is the real-number type in RS-native units, scale(k) returns φ^k for rung index k, and m_p is the proton mass expressed as valence contribution plus binding energy.
proof idea
The definition is a direct string literal assignment; no lemmas or tactics are applied.
why it matters
The definition completes the module summary on RS running couplings by addressing the Landau pole. It sits alongside the listed items on φ-ladder scales, QCD asymptotic freedom, and dimensional transmutation. It touches the framework question of how discreteness at the Planck scale resolves QFT ultraviolet divergences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.