hawking_temperature_one_statement
plain-language theorem explainer
The declaration establishes that in RS-native units the Hawking temperature of a Schwarzschild black hole is T_H(M) = 1/(8 π M), positive for M > 0, strictly decreasing in M, and satisfying T_H(M) t_Page(M) = 640 M². A researcher working on black hole thermodynamics in Recognition Science cites it for the direct link between temperature and horizon rung counting. The proof is a term-mode construction that packages four already-proved component lemmas.
Claim. In RS-native units where c = G = ℏ = k_B = 1, the Hawking temperature of a Schwarzschild black hole satisfies T_H(M) = 1/(8 π M) for mass M. For M > 0 one has T_H(M) > 0. If 0 < M_1 < M_2 then T_H(M_2) < T_H(M_1). The product with Page time obeys T_H(M) · t_Page(M) = 640 M².
background
The module works in RS-native units (c = G = ℏ = k_B = 1) and defines T_hawking(M) := 1/(8 π M), equivalently 1/(4 π r_s) with r_s = 2M the Schwarzschild radius. The Page time is defined as t_Page(M) := 5120 π M³, obtained by integrating the evaporation law dM/dt = −1/M². The local setting is the rung-spacing interpretation on the horizon recognition lattice, where each unit of area carries one ledger rung (the same counting that yields S_BH = A/4 in BlackHoleEntropyFromLedger). Upstream, mass_lt_implies_temp_gt proves lighter holes are hotter by direct positivity and field-simp arithmetic, while temp_times_page_eq_M_sq establishes the structural identity T_H t_Page = 640 M² that recovers the M² area scaling.
proof idea
The proof is a term-mode construction that directly returns the four-tuple of lemmas T_hawking_def, T_hawking_pos, mass_lt_implies_temp_gt, and temp_times_page_eq_M_sq. No further tactics are applied; the conjunction is assembled from the already-established closed-form, positivity, monotonicity, and product results.
why it matters
The theorem consolidates the Hawking temperature identities that support the rung-counting argument in BlackHoleEntropyFromLedger, realizing the RS reading that temperature is the inverse per-rung action quantum on the horizon lattice. It is consistent with the eight-tick octave and D = 3 spatial dimensions from the forcing chain (T0–T8). The result remains conditional on the dimensional bridge from RS-native units to SI, leaving open the explicit matching of the RS-native mass M to physical scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.