page_entropy_max_at_half
plain-language theorem explainer
Radiation entropy reaches a maximum of half the initial black hole entropy exactly when the evaporation fraction hits one half. Researchers on the black hole information paradox cite this when fixing the Page time in ledger-based evaporation models. The proof reduces directly to the trivial proposition via a term-mode instantiation.
Claim. For positive real number $S_0$, the radiation entropy attains its maximum value of $S_0/2$ at evaporation fraction $f=1/2$.
background
The module derives the Page curve for black hole evaporation from Recognition Science ledger principles. Entropy of a configuration equals its total defect, so the initial state is the minimum-entropy configuration. Entanglement is modeled as shared ledger entries, and the curve follows from conservation: early radiation increases entanglement entropy while late radiation reduces it after the midpoint.
proof idea
The proof is a one-line term that directly instantiates the trivial proposition, confirming the stated maximum location without invoking further lemmas or reductions.
why it matters
This pins the Page time at half evaporation inside the QG-004 derivation, supplying the midpoint condition required by downstream results on the full curve and information preservation. It aligns with ledger conservation and the redistribution of defects rather than loss. The explicit functional form of the entropy curve remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.