Quantum Bekenstein Hawking

Black hole thermodynamics

Black hole thermodynamics is the study of black holes as objects with temperature, entropy, and other thermal properties. In 1974, Stephen Hawking showed that quantum effects cause a black hole to radiate particles, giving it a temperature inversely proportional to its mass. Earlier, in 1972, Jacob Bekenstein proposed that a black hole's entropy, a measure of its hidden information, is proportional to the area of its event horizon, not its volume. These two results together form the Bekenstein-Hawking formulas: the entropy S = k_B A / (4 l_P²), where A is horizon area and l_P is the Planck length, and the Hawking temperature T = ℏ c³ / (8π G M k_B), where M is mass. The temperature formula implies a solar-mass black hole radiates at about 6 × 10⁻⁸ kelvin, far colder than the cosmic microwave background, so such holes grow instead of shrinking today. A black hole of one gram, however, would be hot enough to evaporate in a flash.

The formulas carry a deep consequence: a black hole's entropy is enormous, roughly 10⁷⁷ bits for a solar mass, yet it depends only on surface area, not on what fell in. This is the holographic principle, the idea that the information content of a region scales with its boundary, not its volume. The same principle appears in the framework's account, where the horizon area measures the capacity of a discrete ledger, a record of recognition events. In this view, the black hole's entropy counts the ledger's possible states, and the temperature emerges from the scale of the ledger's ticks at the horizon. The framework's library, a machine-checked collection of formal theorems, defines these quantities and proves basic relations among them, such as the entropy being proportional to area and the temperature being inversely proportional to mass.

In Recognition Science, the ledger, a discrete record of events, is the primitive object from which physical structure is derived. The framework models the black hole as a structure with a positive mass, from which it defines the Schwarzschild radius, horizon area, entropy in bits, Hawking temperature, and evaporation time. It proves the entropy-area proportionality as a definitional identity, and it proves that doubling the mass halves the temperature. The framework also states a falsifier structure: if entropy were not area-proportional, or a different temperature law held, or information were lost, the framework's account would be refuted. The module lists predictions, including entropy proportional to area, temperature inversely proportional to mass, information preserved in Hawking radiation, and no firewall at the horizon.

The framework's contribution is to derive these thermodynamic laws from its information-theoretic starting point, not from quantum field theory in curved spacetime. The classical formulas are reproduced, not contradicted. The framework's library proves the algebraic relations among the defined quantities, though the physical derivation from the ledger to the horizon is a stated target, not a completed theorem. The evaporation time for a black hole, proportional to the cube of its mass, is defined in the module as well, giving a concrete lifetime for a black hole of given mass.

/-- The Bekenstein-Hawking entropy S_BH = k_B A / (4 l_P²).

    This is the maximum entropy that can fit in a region
    bounded by area A. It's proportional to AREA, not volume! -/
noncomputable def bekensteinHawkingEntropy (bh : BlackHole) : ℝ :=
  k_B * horizonArea bh / (4 * planckArea)

/-- **THEOREM**: Entropy is proportional to area. -/
theorem entropy_proportional_to_area (bh : BlackHole) :
    bekensteinHawkingEntropy bh = k_B * horizonArea bh / (4 * planckArea) := rfl

/-- **THEOREM**: Hawking temperature is inversely proportional to mass. -/
theorem temperature_inverse_mass (bh1 bh2 : BlackHole)
    (h : bh1.mass = 2 * bh2.mass) :
    hawkingTemperature bh1 = hawkingTemperature bh2 / 2 := by
  unfold hawkingTemperature
  rw [h]
  ring

theorem temperature_from_surface_gravity (bh : BlackHole) :
    hawkingTemperature bh = hbar * surfaceGravity bh / (2 * Real.pi * k_B * c) := by
  unfold hawkingTemperature surfaceGravity
  -- T_H = ℏc³/(8πGMk_B) = ℏ/(2πk_Bc) × c⁴/(4GM) = ℏκ/(2πk_Bc)
  have hM_pos : bh.mass > 0 := bh.mass_pos
  have hc_pos : c > 0 := c_pos
  have hG_pos : G > 0 := G_pos
  have hk_pos : k_B > 0 := by unfold k_B; norm_num
  have hpi_pos : Real.pi > 0 := Real.pi_pos
  have hhbar_pos : hbar > 0 := hbar_pos
  have h_denom_ne : 4 * G * bh.mass ≠ 0 := by positivity
  have h_denom_ne' : 2 * Real.pi * k_B * c ≠ 0 := by positivity
  have h_denom_ne'' : 8 * Real.pi * G * bh.mass * k_B ≠ 0 := by positivity
  field_simp
  ring

/-- The derivation would be falsified if:
    1. Entropy scales with volume, not area
    2. Hawking radiation has different temperature
    3. Information is actually lost -/
structure BHThermodynamicsFalsifier where
  entropy_not_area : Prop
  different_temperature : Prop
  information_lost : Prop
  falsified : entropy_not_area ∨ different_temperature ∨ information_lost → False

What this page does not claim

The framework does not prove that Hawking radiation exists in the physical universe; it defines the temperature and derives relations among its own quantities. The module does not derive the holographic principle from the ledger; it states that the horizon area measures the ledger's information capacity as a modeling choice. No claim is made that the framework's evaporation time matches an observed black hole lifetime, since no such observation exists.

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/BekensteinHawking.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: