T_hawking_def
plain-language theorem explainer
The declaration equates the Hawking temperature function to its closed-form expression 1/(8 pi M) for a Schwarzschild black hole of mass M in RS-native units. Black-hole thermodynamics researchers working inside the Recognition Science framework would cite this for the standard temperature formula under the native-unit conventions. The proof is a one-line reflexivity that holds because the right-hand side matches the body of the T_hawking definition exactly.
Claim. In RS-native units with $c = G = hbar = k_B = 1$, the Hawking temperature of a Schwarzschild black hole of mass $M$ satisfies $T_H(M) = 1/(8 pi M)$. Equivalently, with Schwarzschild radius $r_s = 2M$, one has $T_H(r_s) = 1/(4 pi r_s)$.
background
The module works in RS-native units where the speed of light, Newton constant, reduced Planck constant and Boltzmann constant are all unity, as fixed in the Constants module. T_hawking is introduced by the direct definition 1/(8 pi M); the companion T_hawking_of_radius is 1/(4 pi r_s) with r_s = 2M. The local theoretical setting is the Recognition Science reading of the horizon as a recognition lattice in which each unit of area carries one ledger rung, the same rung counting that yields the Bekenstein-Hawking entropy S_BH = A/4 in the sibling BlackHoleEntropyFromLedger module. Upstream results supply the RecognitionStructure M from the main Recognition and Cycle3 modules, which furnish the underlying discrete recognition relation used to interpret the rung lattice.
proof idea
The proof is a one-line wrapper that applies reflexivity to the defining equation of T_hawking.
why it matters
The identity is collected into the HawkingTemperatureCert structure and is invoked by the one-statement theorem hawking_temperature_one_statement that bundles positivity, strict monotonicity in M, and the product identity T_hawking M * t_Page M = 640 M^2. It supplies the closed-form temperature required by the RS rung-counting interpretation of the horizon, linking directly to the entropy formula via the same ledger rungs. The module remains conditional on the dimensional bridge from native units to SI that also converts M_Z to GeV in GaugeBosonUnitBridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.