Scattering Amplitudes Are Constructively Computable: Bhabha Scattering, Feynman Integrals, and the Fixed-Order Cross Section in BISH (Paper 34, Constructive Reverse Mathematics Series)

Paper 34 in the Constructive Reverse Mathematics of Mathematical Physics series. This paper proves that fixed-order scattering cross sections --- the quantities directly measured at particle collider experiments --- are fully BISH-computable (constructive, no omniscience). A six-tier stratification classifies every operation in a standard QED calculation: tree-level amplitudes (BISH), dilogarithm and special functions (BISH), dimensional regularization with MS-bar subtraction (BISH), Bloch-Nordsieck infrared cancellation (BISH), the inclusive fixed-order cross section (BISH, the main result), and all-orders perturbative summation (LPO via bounded monotone convergence). The result implies that every number a collider experiment actually reports lives in BISH --- the classical-logic cost of particle physics is entirely an artifact of attempting to sum an infinite perturbative series, not of computing any individual prediction. 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