T_hawking
plain-language theorem explainer
The definition supplies the Hawking temperature T_H as 1 over 8 pi M for Schwarzschild mass M in Recognition Science native units. Researchers deriving black hole evaporation rates or Page times from the Recognition framework would reference this expression. It enters as a direct abbreviation of the standard formula after setting c = G = ℏ = k_B = 1.
Claim. $T_H(M) = 1/(8 π M)$ for Schwarzschild mass $M$ in RS-native units (where $c = G = ℏ = k_B = 1$).
background
The module establishes Hawking temperature in RS-native units where c = G = ℏ = k_B = 1. In this setting the standard expression T_H = ℏ c³ / (8 π G M k_B) reduces directly to the given form. The RS reading ties each unit of horizon area to one ledger rung, the same counting that produces Bekenstein-Hawking entropy S_BH = A/4 in the companion ledger module. Upstream structures such as LedgerFactorization supply the J-cost calibration and ContinuumBridge supplies the Laplacian action identification used to interpret the rung lattice.
proof idea
This declaration is introduced as a direct definition that matches the collapsed form of the Hawking formula in RS-native units.
why it matters
It supplies the base expression for the one-statement theorem on Hawking temperature and the certification structure that recovers the M squared scaling of the product with Page time, aligning with the rung-counting entropy in BlackHoleEntropyFromLedger. The module situates this within the dimensional bridge from RS units and the eight-tick octave structure. Downstream results use the definition to prove positivity, strict monotonicity, and the cube-law Page time scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.