pageTime
plain-language theorem explainer
The definition pageTime fixes the dimensionless Page time fraction at exactly one half, the evaporation point where radiation entropy reaches its maximum before declining in the Recognition Science ledger model. Black hole information researchers cite it when proving the tent-shaped Page curve and the associated entropy bound. The declaration is a direct constant assignment requiring no lemmas or computation.
Claim. The Page time fraction is defined by $t_P = 1/2$, the evaporation fraction at which half the initial black hole entropy has been radiated and the radiation entropy reaches its peak.
background
The Quantum.PageCurve module derives the Page curve for black hole evaporation from Recognition Science ledger conservation, where entanglement entropy corresponds to shared defect entries. Entropy of a configuration is proportional to its total defect, with the initial state at minimum entropy. The module treats the curve as a tent function: linear growth before the Page time and linear decline afterward, following from conservation of ledger information.
proof idea
Direct definition that assigns the constant value one half. No lemmas or tactics are invoked; the declaration serves as a primitive fraction for downstream entropy calculations.
why it matters
This supplies the critical fraction used in the Black Hole Information Preservation theorems, including black_hole_information_one_statement and entropy_bound_by_initial_BH_half, which establish that radiation entropy never exceeds the initial black hole entropy divided by two and that joint von Neumann entropy remains zero. It completes the QG-004 target of deriving the Page curve from ledger dynamics, linking to the framework's claim that information is redistributed rather than lost. It touches the open question of firewall avoidance during evaporation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.