surfaceGravity
plain-language theorem explainer
Surface gravity for a Schwarzschild black hole of mass M is defined by the expression κ = c⁴/(4 G M). Workers on black hole thermodynamics in Recognition Science cite this when linking surface gravity to Hawking temperature via T = ℏ κ / (2π k_B c). The definition is a direct algebraic instantiation of the standard GR formula using the RS-native constants c and G.
Claim. For a black hole with positive mass $M$, the surface gravity is defined by $κ = c^4 / (4 G M)$.
background
The Bekenstein-Hawking module derives black hole thermodynamics from Recognition Science, targeting entropy proportional to horizon area and temperature inversely proportional to mass. The BlackHole structure is a record containing a positive real mass field. The constant G is supplied by the RS-native definition G = λ_rec² c³ / (π ℏ) from Constants, with supporting reparametrizations in log coordinates from JCostInflaton where G(t) = cosh(t) - 1.
proof idea
One-line definition that directly encodes the standard general-relativistic surface-gravity formula for a Schwarzschild black hole. It references the imported constants c and G together with the mass field of the BlackHole argument; no auxiliary lemmas or tactics are invoked.
why it matters
The definition supplies the surface-gravity term required by the downstream theorem temperature_from_surface_gravity, which recovers the Hawking temperature T_H = ℏ c³ / (8π G M k_B). It completes the QG-002 step in the module by furnishing the bridge from mass to temperature, consistent with the holographic bound on information capacity at the horizon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.