bulkCapacity_at_one
plain-language theorem explainer
At full evaporation (fraction t = 1), bulk Hilbert-space entropy capacity is identically zero for any black-hole entropy S_BH. Gravity and Page-curve workers cite it as the terminal bulk bound. The proof is a one-line simp unfolding of the linear capacity definition.
Claim. For every real black-hole entropy $S_{\mathrm{BH}}$, the bulk entropy capacity at evaporation fraction $t = 1$ equals zero: $S_{\mathrm{BH}}\cdot(1-1) = 0$.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterised by a fraction $t \in [0,1]$: $t = 0$ is the initial black hole and $t = 1$ is complete evaporation.
Bulk capacity is the linear decrease of available bulk Hilbert-space entropy, defined by $\mathrm{bulkCapacity}(S_{\mathrm{BH}}, t) = S_{\mathrm{BH}}\cdot(1-t)$. It starts at $S_{\mathrm{BH}}$ and reaches zero when the bulk has fully evaporated. The dual radiation capacity grows as $S_{\mathrm{BH}}\cdot t$. Under unitary evolution from a pure initial state, Schmidt purification forces the radiation entropy to equal $\min$ of the two capacities, which is the triangular Page curve.
This lemma records the terminal value of the bulk side of that pair.
proof idea
One-line wrapper: simp [bulkCapacity] unfolds the definition $S_{\mathrm{BH}}\cdot(1-t)$ at $t = 1$ and reduces $1-1$ to $0$, yielding the identity.
why it matters
Feeds pageCurveFromUnitarity_at_one, which shows that the unitarity-derived Page curve returns to zero at full evaporation: after rewriting both capacity endpoints, the min collapses to zero under nonnegativity of $S_{\mathrm{BH}}$. That terminal vanishing is half of the triangular shape forced by Schmidt balance (peak at $t = 1/2$, return to zero at $t = 1$).
In the Gravity Track 3.C programme this closes the kinematic gap left by Session 101's hand-drawn ansatz: the curve is no longer postulated but read off capacity bounds. Within Recognition Science gravity, it is a structural ledger identity, not an RS-constant claim; it does not invoke the forcing chain T0–T8 or the mass ladder, but supplies the bulk endpoint needed for the dynamical Page-curve theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.