radiationCapacity_at_one
plain-language theorem explainer
At full evaporation (fraction t = 1), the radiation Hilbert-space capacity equals the initial black-hole entropy S_BH. Anyone citing the dynamical Page-curve endpoint or the unitarity check at complete evaporation needs this boundary value. The proof is a one-line simplification of the linear definition radiationCapacity = S_BH · t.
Claim. For any real black-hole entropy $S_{\mathrm{BH}}$, the radiation capacity at evaporation fraction $t = 1$ equals $S_{\mathrm{BH}}$: $\mathrm{radCap}(S_{\mathrm{BH}}, 1) = S_{\mathrm{BH}}$.
background
Module Gravity.PageCurveDynamical 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$ one has a pure 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{radCap}(S_{\mathrm{BH}}, t) := S_{\mathrm{BH}} \cdot t$, rising from $0$ at $t = 0$ to $S_{\mathrm{BH}}$ at $t = 1$. The companion bulk capacity shrinks as $S_{\mathrm{BH}} \cdot (1 - t)$. Under unitary evolution from a pure initial state, the joint bulk–radiation state remains pure, so Schmidt forces equal reduced entropies bounded by $\min$ of the two capacities.
This lemma records the right-hand endpoint of that linear radiation ramp.
proof idea
One-line term proof. Unfold the definition $\mathrm{radCap}(S_{\mathrm{BH}}, t) = S_{\mathrm{BH}} \cdot t$ and simplify at $t = 1$, which yields $S_{\mathrm{BH}} \cdot 1 = S_{\mathrm{BH}}$. No external lemmas beyond the definition and arithmetic simplification.
why it matters
Feeds directly into pageCurveFromUnitarity_at_one, which shows that the unitarity-derived Page curve returns to zero at full evaporation: after rewriting both capacities at $t = 1$, one obtains $\min(0, S_{\mathrm{BH}}) = 0$ (for $S_{\mathrm{BH}} \ge 0$). That endpoint is the dynamical counterpart of information recovery: once the bulk capacity has vanished, radiation entropy must fall back to zero under purity of the joint state.
In the module's recipe this closes step 3 of the dynamical construction (linear growth of radiation capacity) at the right boundary, pairing with the bulk-capacity-at-one vanishing lemma. Together they force the triangular shape's return to zero without a kinematic ansatz. The result is pure structural bookkeeping inside Track 3.C; it does not itself invoke RS forcing-chain landmarks (T5–T8) or the mass ladder, but it is part of the gravity-side closure that those foundations ultimately underwrite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.