t_Page_def
plain-language theorem explainer
Page time for a Schwarzschild black hole scales as 5120 π M³ in RS-native units. Physicists modeling black hole evaporation timelines cite this cubic law. The proof reduces immediately to the definition of t_Page by reflexivity.
Claim. $t_{Page}(M) = 5120 π M^3$ for real $M$.
background
The module derives Hawking temperature and Page time from rung spacing on the horizon lattice in Recognition Science. Page time t_Page(M) marks the moment when half the black hole's information has been emitted. In native units the evaporation law dM/dt = -1/M² integrates to the M³ scaling, with prefactor 5120 π taken from the 1976 Page calculation. Upstream, t_Page is introduced as the explicit cubic expression, while Recognition.M supplies the underlying structure.
proof idea
One-line wrapper that applies reflexivity to the definition of t_Page.
why it matters
It supplies the explicit form required by the HawkingTemperatureCert structure, which bundles the temperature and Page-time identities. The M³ scaling closes the integration of the evaporation rate and aligns with the M² area scaling of Bekenstein-Hawking entropy. This step completes the structural identities listed in the module documentation for Track G2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.