temperature_from_surface_gravity
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.