The Physical Dispensability of the Fan Theorem: BISH+LPO Suffices for All Empirical Content of Compact Optimization and Variational Mechanics (A Lean 4 Formalization, Paper 30)

Papers 23 and 28 established that compact optimization (the Extreme Value Theorem on a, b) and variational action minimization in classical mechanics each cost exactly the Fan Theorem (FT) over BISH. Paper 29 established that Fekete’s Subadditive Lemma is equivalent to LPO, and that LPO is physically instantiated because phase transitions are real. This raises the question: is FT an independent physical requirement, or is its cost an artifact of the variational proof method? We prove that every empirically accessible prediction derived from the FT-calibrated results in Papers 23 and 28 is recoverable in BISH+LPO, without invoking the Fan Theorem. The argument rests on three facts: LPO implies bounded monotone convergence (BMC), which yields the supremum and ε-approximate witnesses for any continuous function on a, b; the equations of motion (Euler–Lagrange equations) are BISH-valid and do not require any minimizer to exist; and no finite experiment can distinguish an exact minimizer from an ε-approximate one. Together: FT captures exact existence of an optimizer, while LPO captures convergent approximation to the supremum. Since laboratory measurement has finite precision, FT is physically dispensable. This paper and Paper 31 (Physical Dispensability of Dependent Choice) are released simultaneously. Together with Paper 29, they support the thesis that the logical constitution of empirically accessible physics is BISH+LPO. Lean verification: 918 lines across 7 source files, with zero sorry. Axiom profile: bmcₒfₗpo (cited from Ishihara 2006) is the sole custom axiom used for the core dispensability result. 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. 18638400 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