Observable-Dependent Logical Cost: WLPO and 1D Ising Magnetization Phase Classification

Paper 20: 1D Ising Magnetization and WLPO Title: Observable-Dependent Logical Cost: WLPO and 1D Ising Magnetization Phase Classification Description:Paper 20 in the Constructive Reverse Mathematics (CRM) of Mathematical Physics series. This paper proves that classifying the magnetization phase of the 1D Ising model — determining whether m(∞, β, h) = 0 or m(∞, β, h) ≠ 0 — is equivalent to WLPO (Weak Limited Principle of Omniscience) over BISH. Since the same 1D Ising model has LPO cost for free energy (Paper 8) and WLPO cost for magnetization, this is the first demonstration that logical cost is observable-dependent, not system-dependent. The same physical system exhibits stratified constructive costs (BISH / WLPO / LPO) depending on which quantity is computed. Lean 4 formalization (Mathlib, v4.28.0-rc1): 494 lines, 0 errors, 0 warnings, 0 sorry. Keywords: constructive reverse mathematics, 1D Ising model, magnetization, WLPO, phase classification, observable-dependent cost, Lean 4, Mathlib Complete Paper List Other papers in the Constructive Reverse Mathematics Series (see Zenodo for current files): Paper 1: WithdrawnPaper 2: Bidual gap and WLPO — DOI: 10.5281/zenodo.17107493Paper 3: WithdrawnPaper 4: Quantum spectra axiom calibration — DOI: 10.5281/zenodo.17059483Paper 5: Schwarzschild curvature verification — DOI: 10.5281/zenodo.18489703Paper 6: Heisenberg uncertainty (v2, CRM over Mathlib) — DOI: 10.5281/zenodo.18519836Paper 7: Physical bidual gap, trace-class operators — DOI: 10.5281/zenodo.18527559Paper 8: 1D Ising model and LPO — DOI: 10.5281/zenodo.18516813Paper 9: Ising formulation-invariance — DOI: 10.5281/zenodo.18517570Paper 10: Logical geography of mathematical physics — DOI: 10.5281/zenodo.18580342 v 2.0 Technical Synthesis of Papers 1–16Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10.5281/zenodo.18527676Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18581707 v 2.0 Historical Synthesis of Papers 1–16Paper 13: Event horizon as logical boundary — DOI: 10.5281/zenodo.18529007Paper 14: Quantum decoherence — DOI: 10.5281/zenodo.18569068Paper 15: Noether theorem — DOI: 10.5281/zenodo.18572494Paper 16: Technical note: Born rule — DOI: 10.5281/zenodo.18575377Paper 17: Bekenstein-Hawking formula — DOI: 10.5281/zenodo.18597306Paper 18: Fermion mass hierarchy and scaffolding principle — DOI: 10.5281/zenodo.18600243Paper 19: WKB tunneling and LLPO — DOI: 10.5281/zenodo.18602596Paper 20: Observable-dependent logical cost, 1D Ising magnetization and WLPO — DOI: 10.5281/zenodo.18603079Paper