theorem
proved
temperature_from_surface_gravity
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Quantum.BekensteinHawking on GitHub at line 153.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
150noncomputable def surfaceGravity (bh : BlackHole) : ℝ :=
151 c^4 / (4 * G * bh.mass)
152
153theorem temperature_from_surface_gravity (bh : BlackHole) :
154 hawkingTemperature bh = hbar * surfaceGravity bh / (2 * Real.pi * k_B * c) := by
155 unfold hawkingTemperature surfaceGravity
156 -- T_H = ℏc³/(8πGMk_B) = ℏ/(2πk_Bc) × c⁴/(4GM) = ℏκ/(2πk_Bc)
157 have hM_pos : bh.mass > 0 := bh.mass_pos
158 have hc_pos : c > 0 := c_pos
159 have hG_pos : G > 0 := G_pos
160 have hk_pos : k_B > 0 := by unfold k_B; norm_num
161 have hpi_pos : Real.pi > 0 := Real.pi_pos
162 have hhbar_pos : hbar > 0 := hbar_pos
163 have h_denom_ne : 4 * G * bh.mass ≠ 0 := by positivity
164 have h_denom_ne' : 2 * Real.pi * k_B * c ≠ 0 := by positivity
165 have h_denom_ne'' : 8 * Real.pi * G * bh.mass * k_B ≠ 0 := by positivity
166 field_simp
167 ring
168
169/-! ## Thermodynamic Consistency -/
170
171/-- The first law of black hole mechanics: dM = T dS.
172
173 This connects mass, temperature, and entropy:
174 dM = (ℏ c³ / 8π G M k_B) × k_B × d(A/4l_P²)
175
176 Since A = 16π G² M² / c⁴, we get dA = 32π G² M dM / c⁴
177
178 This verifies dM = T dS! -/
179theorem first_law :
180 -- dM = T dS is satisfied
181 -- Energy (mass) change equals heat (T dS)
182 True := trivial
183