temp_times_page_eq_M_sq
plain-language theorem explainer
The structural identity equates the product of Hawking temperature and Page time for Schwarzschild mass M to 640 M squared in RS-native units. Researchers deriving black-hole thermodynamics from Recognition Science rung counting cite this to recover the area scaling of Bekenstein-Hawking entropy. The proof unfolds the explicit definitions of temperature and Page time then reduces the rational expression by field simplification followed by ring normalization.
Claim. For every real number $M > 0$, if $T_H(M) = 1/(8 π M)$ denotes the Hawking temperature and $t_{Page}(M) = 5120 π M^3$ the Page time, then $T_H(M) · t_{Page}(M) = 640 M^2$.
background
In the Recognition Science treatment of gravity the Hawking temperature is defined as $T_{hawking}(M) = 1/(8 π M)$ in units where $c = G = ℏ = k_B = 1$. The Page time is the evaporation timescale $t_{Page}(M) = 5120 π M^3$ obtained by integrating the mass-loss law $dM/dt = -1/M^2$. This module establishes the closed forms together with positivity and monotonicity before proving the product identity. The local setting is the dimensional bridge from RS-native units to SI, with temperature arising as the reciprocal of the per-rung action quantum on the horizon lattice. Each unit of horizon area carries one ledger rung, linking directly to the entropy formula $S_{BH} = A/4$. Upstream the definitions of $T_{hawking}$ and $t_{Page}$ supply the explicit expressions used here.
proof idea
The proof is a direct algebraic reduction. It unfolds the definitions of $T_{hawking}$ and $t_{Page}$, records that $M ≠ 0$ and π ≠ 0, then applies field_simp to clear denominators followed by ring to normalize the resulting polynomial identity.
why it matters
This identity completes the structural certificate for Hawking temperature. It is invoked by the master certificate structure HawkingTemperatureCert and by the one-statement summary theorem hawking_temperature_one_statement. The $M^2$ scaling recovers the horizon-area dependence of Bekenstein-Hawking entropy, consistent with rung-counting in BlackHoleEntropyFromLedger. Within the Recognition framework it supplies the gravitational sector with the expected thermodynamic scaling that parallels the T5 J-uniqueness and T8 D=3 landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.