What question did this study set out to answer?

The aim is to calibrate the Bekenstein-Hawking entropy formula within the framework of loop quantum gravity using constructive reverse mathematics.

February 13, 2026Open Access

Axiom Calibration of Black Hole Entropy: Spin Network State Counting and the Bekenstein-Hawking Formula

Key Points

The aim is to calibrate the Bekenstein-Hawking entropy formula within the framework of loop quantum gravity using constructive reverse mathematics.
Applied CRM calibration to loop quantum gravity's entropy formula derivation.
Decomposed the formalization into three tiers: BISH, LPO, and subleading logarithmic correction.
Utilized Lean 4 for formalization with error-free implementation.
Demonstrated computability of spin network state counting for certain polynomial barriers.
Proved that leading-order entropy density converges via Bounded Monotone Convergence.
Investigated a subleading logarithmic correction with constructive content.

Abstract

Paper 17: Bekenstein-Hawking Formula Title: Axiom Calibration of Black Hole Entropy: Spin Network State Counting and the Bekenstein-Hawking Formula Description:Paper 17 in the Constructive Reverse Mathematics (CRM) of Mathematical Physics series. This paper applies CRM calibration to loop quantum gravity's derivation of the Bekenstein-Hawking entropy formula S = A/4. The formalization decomposes into three tiers: Part A (BISH) shows that for specific polynomial barriers with algebraically known parameters, the spin network state counting is fully computable; Part B (LPO) demonstrates that the assertion that the leading-order entropy density converges to a completed real requires LPO via Bounded Monotone Convergence; Part C investigates the subleading logarithmic correction S(A) = γ₀A/(4γ) − (3/2)log(A) + O(1) for constructive content. This is the first CRM application to quantum gravity. The Lean 4 formalization (Mathlib, v4.28.0-rc1) builds with 0 errors, 0 warnings, 0 sorry. Keywords: constructive reverse mathematics, black hole entropy, Bekenstein-Hawking formula, loop quantum gravity, spin networks, LPO, BISH, 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 21: Bell nonlocality and LLPO — DOI: 10.5281/zenodo.18603251Paper 22: Markov's Principle and radioactive decay — DOI: 10.5281/zenodo.18603503 Note: GitHub repository is not maintained; please see Zenodo for current files.

Axiom Calibration of Black Hole Entropy: Spin Network State Counting and the Bekenstein-Hawking Formula

Key Points

Abstract

Cite This Study