Encyclopedia Quantum Quantum Black Hole Information

ARTICLE 3 claims 2 theorems 1 model

Quantum Black Hole Information

Black holes may destroy information, but a ledger that never forgets an entry offers a way out.

The ledger's answer

The black hole information paradox is a clash between two certainties. General relativity says that anything falling past a black hole's horizon is gone for good, and Hawking's 1970s calculation showed that black holes slowly radiate energy and eventually evaporate. Quantum mechanics insists that information is never destroyed: the wavefunction evolves unitarily, so the exact initial state always determines the final state. If a black hole evaporates into featureless thermal radiation, the information that fell in appears to be lost, which would break unitarity. The paradox is that both theories seem correct, and they cannot both be.

Recognition Science approaches the problem with a different starting point: a ledger, a discrete record of events that is never erased. In this framework, the ledger is fundamental, and a black hole is a compression of that ledger, not a deletion. The horizon does not destroy entries; it packs them more tightly. Each bit of information is encoded in one Planck area, a bound the framework calls the holographic bound. Hawking radiation is then a slow decompression, carrying the information back out in correlations between emitted quanta. The ledger keeps the accounts balanced from start to finish, so the final state remains pure and unitarity survives.

The framework's machine-checked library of formal theorems, called the Indisputable Monolith, formalizes this picture. It defines a black hole by its mass and a ledger as a list of entries whose total information equals the sum of its parts. A theorem proves that adding an entry preserves the total information exactly. The library also shows that the Bekenstein-Hawking entropy is proportional to mass squared, that the information capacity saturates the holographic bound, and that the Hawking temperature is positive. These are definitions and theorems about a model, not measurements of real black holes.

The module also records three predictions as a named structure: the radiation follows the Page curve, there is no firewall at the horizon, and the final state is pure. A falsifier structure names what would disprove each prediction, such as an observation of a firewall. The library asserts these as true statements, but they are not derived from a physical principle; they are choices about what the model predicts. The paradox, in this account, dissolves because the ledger never loses an entry, but that resolution depends entirely on accepting the ledger as the fundamental reality.

What the module does not do is prove that real black holes behave this way. It builds a consistent formal model where information is conserved, and it shows that the model's predictions match the current consensus in theoretical physics, including the Page curve and the absence of firewalls. The physical bridge from the ledger to actual spacetime remains open. The value of the module is that it makes the ledger's promise precise enough to check, and it names exactly what observation would break it.

THEOREM information_preserved_on_infall · IndisputableMonolith/Quantum/BlackHoleInformation.lean
information_preserved_on_infall · IndisputableMonolith/Quantum/BlackHoleInformation.lean:129
/-- **THEOREM**: Information is preserved when falling into a black hole. -/
theorem information_preserved_on_infall (ledger : BlackHoleLedger) (entry : FallingEntry) :
    (addEntry ledger entry).totalInfo = ledger.totalInfo + entry.information := rfl
THEOREM entropy_proportional_to_mass_squared · bh_saturates_holographic · hawking_temperature_pos · IndisputableMonolith/Quantum/BlackHoleInformation.lean
entropy_proportional_to_mass_squared · IndisputableMonolith/Quantum/BlackHoleInformation.lean:68
/-- **THEOREM**: Black hole entropy is proportional to mass squared. -/
theorem entropy_proportional_to_mass_squared (bh : BlackHole) :
    bekensteinHawkingEntropy bh = 4 * Real.pi * bh.mass^2 := by
  unfold bekensteinHawkingEntropy horizonArea
  ring
/-- **THEOREM**: Black hole saturates the holographic bound. -/
theorem bh_saturates_holographic (bh : BlackHole) :
    informationCapacity bh = holographicBound (horizonArea bh) := by
  unfold informationCapacity holographicBound bekensteinHawkingEntropy
  ring
/-- **THEOREM**: Hawking temperature is positive. -/
theorem hawking_temperature_pos (bh : BlackHole) : hawkingTemperature bh > 0 := by
  unfold hawkingTemperature
  apply one_div_pos.mpr
  apply mul_pos
  apply mul_pos
  · norm_num
  · exact Real.pi_pos
  · exact bh.mass_pos
MODEL rsPredictions · IndisputableMonolith/Quantum/BlackHoleInformation.lean
/-- RS predictions. -/
def rsPredictions : BlackHolePredictions := {
  pageCurve := true,
  hasFirewall := false,
  finalPure := true
}

What this page does not claim

No claim that real black holes preserve information, only that a formal ledger model does. No derivation of the Page curve or firewall absence from first principles; these are stated as predictions. No proof that the ledger's compression mechanism corresponds to any known physics.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Quantum/BlackHoleInformation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND