t_Page
plain-language theorem explainer
Page time in RS-native units is defined as 5120 π M³ for black hole mass M. Researchers on black hole evaporation and information in Recognition Science cite this for the cubic scaling obtained by integrating dM/dt = -1/M² to the half-information point. The declaration is a direct algebraic definition that supplies the conventional Page prefactor inside the framework's unit system.
Claim. The Page time satisfies $t_{Page}(M) = 5120 π M^3$ for Schwarzschild black hole mass $M$ in RS-native units.
background
The HawkingTemperatureFromRung module works in RS-native units with c = G = ħ = k_B = 1. Hawking temperature is given by T_H(M) = 1/(8 π M) and equivalently T_H(r_s) = 1/(4 π r_s) with r_s = 2M. Page time is the integrated duration to emit half the black hole information, obtained from the evaporation law dM/dt = -1/M². Upstream Recognition.M supplies the core RecognitionStructure {U, R} that underpins rung counting across the framework, while Cycle3.M instantiates a three-cycle version of the same structure.
proof idea
The declaration is a direct definition with an empty proof body. It encodes the M³ scaling and the numerical Page factor 5120 π without invoking lemmas or tactics.
why it matters
This definition supplies t_Page for the HawkingTemperatureCert structure and for the identity temp_times_page_eq_M_sq, which proves T_H * t_Page = 640 M² and recovers the M² scaling of horizon area and Bekenstein-Hawking entropy S_BH = A/4. It completes the Page-time component of the module's structural identities, linking evaporation dynamics to the rung lattice of BlackHoleEntropyFromLedger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.