The Physical Dispensability of Dependent Choice: A Lean 4 Formalization (Paper 31, Constructive Reverse Mathematics Series)

Paper 31 in the Constructive Reverse Mathematics of Mathematical Physics series. This paper proves that Dependent Choice (DC) is physically dispensable: every empirically accessible prediction derived from DC-calibrated results --- the Strong Law of Large Numbers (SLLN) and the Birkhoff pointwise ergodic theorem --- is recoverable in BISH + LPO without invoking DC. The key insight is that DC is needed only for infinite quantifier swaps that no finite apparatus can perform. The Weak Law of Large Numbers (WLLN) suffices for all SLLN predictions via BISH-computable Chebyshev bounds, and the Mean Ergodic Theorem (MET) suffices for all Birkhoff predictions via LPO modulus extraction. The master theorem establishes that BISH + LPO is the complete logical constitution of empirically accessible physics, with DC, the Fan Theorem, and other strong set-existence principles all dispensable. All results formalized in Lean 4 over Mathlib with zero sorry. The formalization comprises 5 Lean source files. Complete Paper List Complete Paper List Other papers in the Constructive Reverse Mathematics Series (see Zenodo for current files): 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 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