 147    True := trivial
 148
 149/-- The surface gravity κ = c⁴/(4GM) is related to temperature by T = ℏκ/(2π k_B c). -/
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.