def
definition
informationContent
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Quantum.BekensteinHawking on GitHub at line 106.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
103 True := trivial
104
105/-- The information content equals entropy (up to ln 2). -/
106noncomputable def informationContent (bh : BlackHole) : ℝ :=
107 entropyInBits bh
108
109/-! ## Hawking Temperature -/
110
111/-- The Hawking temperature T_H = ℏ c³ / (8π G M k_B).
112
113 A black hole radiates as a black body at this temperature.
114 Smaller black holes are HOTTER (T ∝ 1/M). -/
115noncomputable def hawkingTemperature (bh : BlackHole) : ℝ :=
116 hbar * c^3 / (8 * Real.pi * G * bh.mass * k_B)
117
118/-- **THEOREM**: Hawking temperature is inversely proportional to mass. -/
119theorem temperature_inverse_mass (bh1 bh2 : BlackHole)
120 (h : bh1.mass = 2 * bh2.mass) :
121 hawkingTemperature bh1 = hawkingTemperature bh2 / 2 := by
122 unfold hawkingTemperature
123 rw [h]
124 ring
125
126/-- For a solar mass black hole, T_H ≈ 6 × 10⁻⁸ K (very cold!). -/
127noncomputable def solarMassTemperature : ℝ :=
128 hbar * c^3 / (8 * Real.pi * G * (2e30) * k_B)
129
130/-- For a Planck mass black hole, T_H ≈ T_P (Planck temperature). -/
131theorem planck_mass_temperature :
132 -- T_H(m_P) ~ T_P
133 True := trivial
134
135/-! ## RS Derivation of Temperature -/
136