temperature_from_surface_gravity
Physicists working on black hole thermodynamics in Recognition Science cite this result to recover the standard Hawking temperature formula from the module's definitions. For any Schwarzschild black hole with positive mass the equality T_H = ħ κ / (2 π k_B c) holds, where κ is surface gravity. The tactic proof unfolds the two definitions, invokes positivity lemmas for mass, c, G, ħ, k_B and π, then finishes with field_simp and ring.
claimFor a Schwarzschild black hole with positive mass $M$, the Hawking temperature satisfies $T_H = hbar * surfaceGravity / (2 * pi * k_B * c)$, where surfaceGravity denotes the horizon surface gravity.
background
The Quantum.BekensteinHawking module derives black hole thermodynamics from Recognition Science. Hawking temperature is defined as T_H = ħ c³ / (8 π G M k_B) and surface gravity as the corresponding horizon quantity κ = c⁴ / (4 G M). The BlackHole structure is a record containing only a positive real mass field.
proof idea
The tactic proof first unfolds hawkingTemperature and surfaceGravity. It obtains positivity of bh.mass from the structure field, c from c_pos, G from G_pos, ħ from hbar_pos, k_B by norm_num, and π from Real.pi_pos. Three positivity goals clear the denominators, after which field_simp followed by ring reduces the identity.
why it matters in Recognition Science
The theorem supplies the temperature half of the Bekenstein-Hawking pair in the module, immediately preceding the first-law consistency comment dM = T dS. It realizes the module's target of obtaining T_H from the τ₀-scale at the horizon and aligns with the RS constants ħ = φ^{-5} and G = λ_rec² c³ / (π ħ). No downstream uses are recorded.
scope and limits
- Does not treat rotating or charged black holes.
- Does not derive the area-entropy law.
- Does not include quantum corrections to temperature.
- Does not prove surface gravity from ledger dynamics.
formal statement (Lean)
153theorem temperature_from_surface_gravity (bh : BlackHole) :
154 hawkingTemperature bh = hbar * surfaceGravity bh / (2 * Real.pi * k_B * c) := by
proof body
Tactic-mode proof.
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! -/