The Fan Theorem and the Constructive Cost of Optimization: Free Energy Extrema on Compact Parameter Spaces (Paper 23, Constructive Reverse Mathematics Series)

Paper 23 (DOI: 10.5281/zenodo.18604312) Title: The Fan Theorem and the Constructive Cost of Optimization: Free Energy Extrema on Compact Parameter Spaces (Paper 23, Constructive Reverse Mathematics Series) Description: Paper 23 in the Constructive Reverse Mathematics Series. Lean 4 formalization establishing that the Extreme Value Theorem (EVT) — "a continuous function on a compact interval attains its extremum" — is equivalent to the Fan Theorem (FT) over Bishop-style constructive mathematics (BISH). The equivalence is instantiated through free energy optimization in the 1D Ising model. This is the first CRM calibration at the Fan Theorem, adding a third independent branch to the calibration hierarchy (independent of the LPO/WLPO/LLPO omniscience chain). The same physical system — the 1D Ising model — now exhibits four distinct logical costs across Papers 8, 20, 22, and 23: finite-volume computation (BISH), thermodynamic limit (LPO), phase classification (WLPO), and parameter-space optimization (FT). Main results: ft_iff_compact_opt (FanTheorem ↔ CompactOptimization), evt_max_iff_evt_min (EVT_max ↔ EVT_min), ising_opt_of_ft (FT → Ising free energy minimum exists), fan_stratification (three-branch partial order). Axiom audit: ZERO custom axioms — cleanest audit in the series. Bundle contains: LaTeX source and compiled PDF (~20 pages), Lean 4 formalization (14 files, ~684 lines, 0 errors/0 warnings/0 sorry), proof specification, bibliography, and README. Built with Lean 4.28.0-rc1 + Mathlib. Complete Paper List (Papers 1–24) 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.18580342 [v 2.0 Technical Synthesis of Papers 1–16] Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10.5281/zenodo.18527676 Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18581707 [v 2.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: Fermion mass hierarchy and scaffolding principle — DOI: 10.5281/zenodo.18600243 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