pageTime
plain-language theorem explainer
The definition supplies the Page time t_P = M₀/(2α) as half the evaporation time for a black hole with initial mass M₀ and rate α. Physicists working on the information paradox in Recognition Science cite it to locate the midpoint where radiation entropy peaks. It is realized by direct definition matching the half-evaporation condition from the upstream PageCurve module.
Claim. The Page time is defined by $t_P(M_0, α) = M_0 / (2α)$, where $M_0$ is the initial black-hole mass and $α$ is the constant evaporation rate.
background
The module resolves the black-hole information paradox by treating Hawking radiation as unitary emission of recognition rungs from the horizon ledger. The black-hole plus radiation system remains a pure state on the Recognition Hilbert Space at all times, so the joint von Neumann entropy is identically zero and the reduced entropies satisfy S_R(t) = S_BH(t). The Page curve then emerges: radiation entropy grows linearly until the Page time then falls back to zero, never exceeding M₀/8.
proof idea
Direct definition implementing the Page time as half the total evaporation time. It matches the upstream abstract pageTime (evaporation_fraction = 1/2) by substituting the concrete linear profile M(t) = M₀ - α t.
why it matters
This definition anchors the Page time slot in BlackHoleInformationCert and black_hole_information_one_statement, which together assert t_P = t_evap/2, S_thermal = S_BH at t_P, and the bound S_R(t) ≤ M₀/8. It fills the concrete expression needed for the module's Page-curve emergence claim and supports the Recognition Science resolution via joint pure-state invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.