pageEntropy
plain-language theorem explainer
The definition sets the Page entropy to M₀/8 for initial black-hole mass M₀. Researchers resolving the information paradox via the Page curve cite this bound to cap radiation entropy at half the initial Bekenstein-Hawking value. It appears in statements that S_R(t) never exceeds this threshold during linear evaporation. The definition is a direct algebraic assignment with no lemmas or computation.
Claim. The Page entropy is defined by $S_0/2 = M_0/8$, where $M_0$ is the initial black-hole mass and $S_0 = M_0/4$ is the initial Bekenstein-Hawking entropy.
background
In the Recognition Science treatment of black-hole evaporation the module assumes linear mass loss $M(t) = M_0 - α t$ and derives the Page curve from the joint pure-state condition on the black-hole-plus-radiation system. The Page entropy is the peak value of radiation entropy $S_R(t)$ attained at the Page time $t_P = t_{evap}/2$. It equals half the initial entropy because $S_{BH}(t) = M(t)/4$ in RS units, so the maximum is $M_0/8$ when $M(t_P) = M_0/2$ and $S_{thermal}(t_P) = M_0/8$ as well.
proof idea
This is a direct definition that assigns pageEntropy M₀ the value M₀/8. No upstream lemmas are invoked and no tactics are used; the expression is introduced as the constant target for later bounds such as entropy_bound_by_initial_BH_half and S_R_at_page_eq_page_entropy.
why it matters
The definition supplies the explicit numerical bound used inside BlackHoleInformationCert and the one-statement theorem black_hole_information_one_statement. It realizes the Page-bound clause of the G1 track, confirming that radiation entropy stays ≤ M₀/8 while the joint von Neumann entropy remains zero. This closes the information-preservation argument under the pure-state and reduced-entropy-equality assumptions stated in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.