radiationCapacity_at_zero
plain-language theorem explainer
Radiation Hilbert-space entropy capacity vanishes at the start of evaporation: for any black-hole entropy $S_{BH}$, the capacity at fraction $t=0$ is zero. Anyone citing the dynamical Page-curve boundary values or the unitarity-at-zero identity needs this. The proof is a one-line `simp` unfolding of the linear definition.
Claim. For every real black-hole entropy $S_{BH}$, the radiation entropy capacity at evaporation fraction $t=0$ equals zero: $S_{BH}\cdot 0=0$.
background
Module Gravity Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterised by $t\in[0,1]$: the fraction of total entropy transferred from bulk to radiation. At $t=0$ the system is the initial black hole; at $t=1$ evaporation is complete.
Radiation capacity is the entropy capacity of the radiation Hilbert space. By definition it grows linearly: $\mathrm{radiationCapacity}(S_{BH},t)=S_{BH}\cdot t$, from $0$ at $t=0$ to $S_{BH}$ at $t=1$. Bulk capacity shrinks as $S_{BH}\cdot(1-t)$. Under unitary evolution from a pure initial state, Schmidt's theorem forces the radiation entropy to saturate $\min$ of the two capacities, which is the triangular Page curve.
The upstream definition is exactly that linear product. This lemma records the left endpoint of the radiation branch.
proof idea
One-line wrapper: simp unfolds radiationCapacity to the product $S_{BH}\cdot t$ and reduces the $t=0$ case to the ring identity $S_{BH}\cdot 0=0$. No further lemmas are required.
why it matters
Boundary values of the two capacities pin the Page curve at the start and end of evaporation. Downstream, pageCurveFromUnitarity_at_zero rewrites the unitarity-derived Page curve at $t=0$ by applying this fact together with bulk capacity at zero, then concludes $\min(S_{BH},0)=0$ under $S_{BH}\ge 0$. That identity is part of the operator-level Page-process interface: the entropy readout must return zero before any Hawking quanta are emitted.
In the broader Recognition gravity track this closes a kinematic endpoint of the dynamical recipe (steps 1--6 in the module doc). The triangular shape, including return to zero at full evaporation and the forced peak at $t=1/2$, is no longer an ansatz. Microscopic derivation of the entropy readout from a specific Hamiltonian remains open, as the downstream interface doc notes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.