remainingEntropy
plain-language theorem explainer
remainingEntropy computes leftover black hole entropy after partial evaporation by scaling initial entropy by the unevaporated fraction. Researchers deriving the Page curve from ledger conservation cite it to close the late-time branch of radiation entropy. The definition is a direct algebraic scaling of the two fields inside the EvolvingBlackHole structure.
Claim. For an evolving black hole with initial entropy $S_0$ and evaporated mass fraction $f$, the remaining entropy is $S_0(1-f)$.
background
The module derives the Page curve for black hole evaporation from Recognition Science ledger dynamics, where entanglement entropy is tracked via shared defect entries. EvolvingBlackHole is the structure holding initial Bekenstein-Hawking entropy and the evaporation fraction together with positivity and range constraints. Upstream entropy definitions from InitialCondition (proportional to total defect) and from BoltzmannDistribution and PartitionFunction (standard thermodynamic expressions) supply the justification for treating $S_0$ as the relevant entropy measure.
proof idea
The definition is a one-line algebraic expression that multiplies the initial entropy field by the complement of the evaporation fraction field.
why it matters
This definition supplies the decreasing branch of pageEntropy after Page time, completing the linear Page curve that follows from ledger conservation. It directly supports the QG-004 claim that information is preserved by redistribution rather than loss. The construction sits inside the eight-tick octave and phi-ladder framework without additional holographic assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.