pageEntropy
plain-language theorem explainer
The pageEntropy definition computes radiation entanglement entropy for an evolving black hole by returning radiationEntropyNaive when evaporation fraction is at or below pageTime and remainingEntropy otherwise. Physicists addressing the black hole information paradox cite this to recover the tent-shaped Page curve from ledger conservation. The implementation is a direct conditional split on the evaporation fraction.
Claim. For an evolving black hole with initial entropy $S_0$ and evaporation fraction $f$, the radiation entanglement entropy equals $S_0 f$ when $f$ is at most the Page time and $S_0(1-f)$ when $f$ exceeds the Page time.
background
The Quantum.PageCurve module derives the Page curve from entanglement dynamics under Recognition Science, where entanglement equals shared ledger entries and information is conserved by redistribution rather than loss. The EvolvingBlackHole structure records initial Bekenstein-Hawking entropy $S_initial > 0$ together with evaporation fraction in $[0,1]$. Upstream, entropy of a configuration is defined as its total defect, so the initial state is the minimum-entropy configuration.
proof idea
The definition is a direct case split on whether the evaporation fraction is at most pageTime, returning radiationEntropyNaive in the first branch and remainingEntropy in the second. No lemmas are applied beyond the imported pageTime threshold.
why it matters
This definition supplies the radiation entropy function required by BlackHoleInformationCert and the one-statement black hole information preservation theorem. It realizes the QG-004 target of deriving the Page curve from ledger dynamics, as stated in the module's Nature paper proposition. The construction ensures the radiation entropy respects the Page bound $M_0/8$ at half evaporation while preserving the joint pure state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.