radiationEntropyNaive
plain-language theorem explainer
radiationEntropyNaive computes the entropy carried away by radiation as the product of a black hole's initial Bekenstein-Hawking entropy and its evaporated mass fraction. It supplies the linear growth segment of the Page curve in Recognition Science models of evaporation before the turnover. The definition performs direct multiplication on the two fields of the EvolvingBlackHole record.
Claim. For an evolving black hole with initial entropy $S_0$ and evaporated fraction $f$, the naive radiated entropy is $S_0 f$.
background
Recognition Science treats black hole evaporation through ledger conservation, where entanglement entropy counts shared defect entries between the black hole and its radiation. The EvolvingBlackHole structure records the initial Bekenstein-Hawking entropy together with the evaporated fraction subject to the constraints $S_0 > 0$ and $0 ≤ f ≤ 1$. Upstream, entropy is defined as total defect count, yielding zero entropy for the minimum-defect initial state.
proof idea
One-line definition that multiplies the initial entropy field by the evaporation fraction field of the supplied EvolvingBlackHole record.
why it matters
This definition supplies the pre-Page-time branch to pageEntropy, which assembles the full Page curve. It realizes the early-time linear growth segment in the QG-004 derivation of the Page curve from ledger dynamics. The construction supports the information-preservation claim that late radiation restores the initial entropy through entanglement with early quanta.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.