Paper 25 in the Constructive Reverse Mathematics Series. We open a new axis in the constructive reverse mathematics (CRM) calibration of mathematical physics: the choice hierarchy AC₀ < CC < DC. The main result is that the mean ergodic theorem (von Neumann, 1932) is equivalent over BISH to Countable Choice (CC). The forward direction—CC implies the mean ergodic theorem—is fully formalized in Lean 4 with 600+ lines of genuine Hilbert space analysis and a clean axiom profile. For the reverse direction, we introduce a Type-level computable mean ergodic statement and prove it implies CC through an explicit ℓ²(ℕ × ℕ) encoding with a diagonal reflection operator; the hypothesis is genuinely used, not discarded. We further calibrate Birkhoff's pointwise ergodic theorem (1931) to Dependent Choice (DC), the weak law of large numbers to CC, and the strong law of large numbers to DC. The calibration reveals a clean physical separation: ensemble/average behavior requires CC; individual trajectory behavior requires DC. We propose the DC Ceiling Thesis: no calibratable physical theorem requires more than DC. The combined formalization comprises 1805 lines of Lean 4 across 12 modules with zero non-permanent sorries, one custom axiom (Birkhoff's theorem is not in Mathlib4), and two permanent model-theoretic sorries for independence results. Paper 25 in the Constructive Reverse Mathematics series. 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: 110.5281/zenodo.18613542 v 3.0 Technical Synthesis of Papers 1–24Paper 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 21: Bell nonlocality and LLPO — DOI: 10.5281/zenodo.18603251Paper 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 Summary Papers: Paper 10: Logical geography of mathematical physics — DOI: 110.5281/zenodo.18613542 v 3.0 Technical Synthesis of Papers 1–24 Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18581707 v 2.0 Historical Synthesis of Papers 1–16 Note: The GitHub repository is no longer maintained; please see Zenodo for the current files.
Paul Chun-Kit Lee (Wed,) studied this question.