bulkCapacity_at_zero
plain-language theorem explainer
At the start of evaporation (fraction t = 0), bulk Hilbert-space entropy capacity equals the initial black-hole entropy S_BH. Anyone citing the dynamical Page-curve boundary values or the unitarity-at-zero identity needs this evaluation. The proof is a one-line simp unfolding of the linear bulk-capacity definition.
Claim. For every real black-hole entropy $S_{\mathrm{BH}}$, the bulk entropy capacity at evaporation fraction $t = 0$ equals $S_{\mathrm{BH}}$: $C_{\mathrm{bulk}}(S_{\mathrm{BH}}, 0) = S_{\mathrm{BH}}$, where $C_{\mathrm{bulk}}(S_{\mathrm{BH}}, t) := S_{\mathrm{BH}}\,(1 - t)$.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced pure joint states on bulk ⊗ radiation, rather than postulating a piecewise-linear ansatz. Evaporation is parameterised by $t \in [0,1]$: the fraction of total entropy transferred from bulk to radiation.
Bulk capacity is the linear decrease $C_{\mathrm{bulk}}(S_{\mathrm{BH}}, t) = S_{\mathrm{BH}},(1 - t)$, so the bulk Hilbert space shrinks from full black-hole entropy at $t = 0$ to zero at full evaporation. Radiation capacity grows as $S_{\mathrm{BH}}, t$. Under unitarity the joint state stays pure, Schmidt forces equal reduced entropies, and both are bounded by $\min(C_{\mathrm{bulk}}, C_{\mathrm{rad}})$.
The upstream definition states: "Bulk Hilbert-space entropy capacity at evaporation fraction $t$. Linear decrease from $S_{\mathrm{BH}}$ at $t = 0$ to $0$ at $t = 1$." This lemma records the left endpoint of that line.
proof idea
One-line wrapper: simp [bulkCapacity] unfolds $C_{\mathrm{bulk}}(S_{\mathrm{BH}}, t) = S_{\mathrm{BH}},(1 - t)$ at $t = 0$, yielding $S_{\mathrm{BH}},(1 - 0) = S_{\mathrm{BH}}$. No further lemmas are required.
why it matters
Feeds pageCurveFromUnitarity_at_zero, which shows the unitarity-derived Page curve vanishes at $t = 0$: after unfolding, it rewrites with this identity and the matching radiation-capacity-at-zero fact, then applies $\min(S_{\mathrm{BH}}, 0) = 0$ under $S_{\mathrm{BH}} \ge 0$.
That boundary check is part of the dynamical recipe that replaces Session 101's kinematic triangular ansatz with a derived $\min$ of two monotone capacities. The module is marked structural (0 sorry): the Page peak at $t = 1/2$ and return to zero are forced by Schmidt balance, not chosen. Downstream operator-level Page-process work still leaves open deriving the entropy readout from a specific microscopic Hamiltonian; this lemma only pins the bulk endpoint of the ledger-tick curve.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.