radiationCapacity
plain-language theorem explainer
Radiation Hilbert-space entropy capacity grows linearly as S_BH · t with evaporation fraction t. Anyone deriving the dynamical Page curve from Schmidt-balanced bulk⊗radiation transfer cites this as the ascending capacity bound. The definition is the one-line product S_BH * t.
Claim. The radiation entropy capacity at black-hole entropy $S_{\mathrm{BH}}$ and evaporation fraction $t$ is $S_{\mathrm{BH}}\, t$. It rises linearly from $0$ at $t=0$ to $S_{\mathrm{BH}}$ at full evaporation $t=1$.
background
Track 3.C derives the triangular Page curve from Schmidt purification on a pure joint state of bulk and radiation, rather than postulating a piecewise-linear ansatz. Evaporation is parameterized by $t\in[0,1]$: the fraction of total entropy transferred from bulk to radiation.
Bulk capacity shrinks as $S_{\mathrm{BH}}(1-t)$; radiation capacity grows as $S_{\mathrm{BH}}, t$. Unitary evolution from a pure initial bulk state keeps the joint state pure, so Schmidt's theorem forces $S(\rho_{\mathrm{bulk}})=S(\rho_{\mathrm{rad}})$ and both are bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$. Under maximal Schmidt balance the radiation entropy saturates that min bound.
This definition is the ascending leg of that pair of monotone capacities. Its sibling bulk capacity and the sum-invariant theorem close the linear-transfer picture used throughout the module.
proof idea
Pure definition: the body is the product $S_{\mathrm{BH}}\cdot t$. No lemmas or tactics. Downstream proofs unfold it (often together with bulk capacity) and simplify by ring or min rewriting.
why it matters
Without the linear radiation capacity there is no dynamical Page curve: the curve is defined as $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$ under Schmidt balance. The one-statement theorem, the master cert PageCurveDynamicalCert, and the ledger-tick specializations all quote this bound directly.
It also anchors the MasterTheorem handoff endpoint: finite emitted recognition ticks induce the same capacity via radiationCapacityFromTicks, conserving total capacity and recovering the Schmidt min curve at the tick-induced fraction. The peak at $t=1/2$ and return to zero at $t=1$ are forced by the min of this rising line against the falling bulk line, not inserted by hand. That closes Session 101's kinematic gap and supplies the structural half of Gravity Track 3.C.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.