QED One-Loop Renormalization: The Landau Pole --- Constructive Reverse Mathematics of the Running Coupling, Threshold Crossings, and the Landau Divergence (Paper 32, Constructive Reverse Mathematics Series)

Paper 32 in the Constructive Reverse Mathematics of Mathematical Physics series. This paper provides a complete constructive reverse-mathematical calibration of quantum electrodynamics (QED) at one-loop order. The central surprise: the Landau pole divergence --- often presented as a fundamental crisis of QED --- is fully BISH-computable. The closed-form ODE solution for the running coupling constant provides an explicit Cauchy modulus requiring no omniscience principle. Six theorems classify the logical cost of each QED operation: discrete renormalization group steps and coupling below the pole are BISH, the Landau pole divergence itself is BISH, threshold crossing decisions cost WLPO, and global coupling determination costs LPO via bounded monotone convergence. Ward-Takahashi identity preservation is BISH. All results formalized in Lean 4 over Mathlib with zero sorry. The formalization comprises 8 Lean source files. Complete Paper List Other papers in the Constructive Reverse Mathematics Series (see Zenodo for current files): Summary Papers: Paper 10: Logical geography of mathematical physics -- DOI: 10.5281/zenodo.18636180 Paper 12: Constructive history of mathematical physics -- DOI: 10.5281/zenodo.18636250 Series: Paper 1: Withdrawn Paper 2: Bidual gap and WLPO -- DOI: 10.5281/zenodo.17107493 Paper 3: Withdrawn Paper 4: Quantum spectra axiom calibration -- DOI: 10.5281/zenodo.17059483 Paper 5: Schwarzschild curvature verification -- DOI: 10.5281/zenodo.18489703 Paper 6: Heisenberg uncertainty (v2, CRM over Mathlib) -- DOI: 10.5281/zenodo.18519836 Paper 7: Physical bidual gap, trace-class operators -- DOI: 10.5281/zenodo.18527559 Paper 8: 1D Ising model and LPO -- DOI: 10.5281/zenodo.18516813 Paper 9: Ising formulation-invariance -- DOI: 10.5281/zenodo.18517570 Paper 10: Logical geography of mathematical physics -- DOI: 10.5281/zenodo.18627193 Paper 11: Entanglement, CHSH, Tsirelson bound -- DOI: 10.5281/zenodo.18527676 Paper 12: Constructive history of mathematical physics -- DOI: 10.5281/zenodo.18627283 v2.0 Historical Synthesis of Papers 1-16 Paper 13: Event horizon as logical boundary -- DOI: 10.5281/zenodo.18529007 Paper 14: Quantum decoherence -- DOI: 10.5281/zenodo.18569068 Paper 15: Noether theorem -- DOI: 10.5281/zenodo.18572494 Paper 16: Technical note: Born rule -- DOI: 10.5281/zenodo.18575377 Paper 17: Bekenstein-Hawking formula -- DOI: 10.5281/zenodo.18597306 Paper 18: Constructive Stratification of the Standard Model Yukawa RG -- DOI: 10.5281/zenodo.18626839 (version 2) Paper 19: WKB tunneling and LLPO -- DOI: 10.5281/zenodo.18602596 Paper 20: Observable-dependent logical cost, 1D Ising magnetization and WLPO -- DOI: 10.5281/zenodo.18603079 Paper 21: Bell nonlocality and LLPO -- DOI: 10.5281/zenodo.18603251 Paper 22: Markov's Principle and radioactive decay -- DOI: 10.5281/zenodo.18603503 Paper 23: Fan Theorem and optimization -- DOI: 10.5281/zenodo.18604312 Paper 24: Kochen-Specker contextuality and LLPO -- DOI: 10.5281/zenodo.18604317 Paper 25: Ergodic Theorems and Laws of Large Numbers against Countable and Dependent Choice -- DOI: 10.5281/zenodo.18615453 Paper 26: Bidual Gap Detection Is WLPO-Complete: Godel Sequences -- DOI: 10.5281/zenodo.18615457 Paper 27: IVT as the mechanism behind LLPO in Bell physics -- DOI: 10.5281/zenodo.18615459 Paper 28: Classical Mechanics -- DOI: 10.5281/zenodo.18616620 Paper 29: Fekete's Subadditive Lemma -- DOI: 10.5281/zenodo.18643617 Paper 30: Physical Dispensability of the Fan Theorem -- DOI: 10.5281/zenodo.18638394 Paper 31: Physical Dispensability of Dependent Choice -- DOI: 10.5281/zenodo.18645578 Paper 32: QED One-Loop Renormalization: The Landau Pole -- DOI: 10.5281/zenodo.18642598 Paper 33: QCD One-Loop Renormalization and Confinement -- DOI: 10.5281/zenodo.18642610 Paper 34: Scattering Amplitudes Are Constructively Computable -- DOI: 10.5281/zenodo.18642612 Paper 35: The Logical Constitution of Empirical Physics -- DOI: 10.5281/zenodo.18642616 Paper 36: Stratifying Spectral Gap Undecidability (Cubitt's Theorem) -- DOI: 10.5281/zenodo.18642620 Paper 37: The Undecidability Landscape Is LPO -- DOI: 10.5281/zenodo.18642802 Paper 38: Wang Tiling and the Origin of Physical Undecidability -- DOI: 10.5281/zenodo.18642804 Paper 39: Beyond LPO: Thermodynamic Stratification of Physical Undecidability -- DOI: 10.5281/zenodo.18642806 QED, one-loop renormalization, Landau pole, running coupling constant, beta function, constructive reverse mathematics, BISH, LPO, WLPO, bounded monotone convergence, threshold crossing, Ward-Takahashi identity, Lean 4, Mathlib, formal verification, renormalization group