bulkCapacity
plain-language theorem explainer
Bulk Hilbert-space entropy capacity falls linearly with evaporation fraction: $S_{BH}(1-t)$, from full horizon entropy at $t=0$ to zero at complete evaporation. Track 3.C Page-curve work cites it as one monotone bound in the Schmidt min that forces the triangle. The body is a one-line product definition; endpoint and tick-bridge lemmas unfold it directly.
Claim. For horizon entropy $S_{BH}\in\mathbb{R}$ and evaporation fraction $t\in\mathbb{R}$, the bulk Hilbert-space entropy capacity is defined by $S_{\mathrm{bulk}}(S_{BH},t):=S_{BH}\,(1-t)$. It decreases linearly from $S_{BH}$ at $t=0$ to $0$ at $t=1$.
background
Module Gravity.PageCurveDynamical (Track 3.C) replaces the Session-101 kinematic triangular ansatz with a derived Page curve. Evaporation is parameterized by $t\in[0,1]$: the fraction of total entropy transferred from bulk to radiation. The joint state on $H_{\mathrm{bulk}}\otimes H_{\mathrm{rad}}$ stays pure under unitary evolution, so Schmidt forces $S(\rho_{\mathrm{bulk}})=S(\rho_{\mathrm{rad}})$ and both are bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$.
Bulk capacity is the shrinking upper bound on bulk entropy as the hole evaporates; the sibling radiation capacity grows as $S_{BH},t$. Horizon entropy $S_{BH}$ is the initial bulk scale (cf. ledger/Boltzmann entropy readings upstream: defect totals, $\log$ of patch microstates). The Page curve is then $\min$ of the two linear capacities under maximal Schmidt entanglement.
proof idea
Definitional one-liner: unfold to the product $S_{BH}\cdot(1-t)$. No tactics or lemmas. Downstream simp lemmas (bulkCapacity_at_zero, bulkCapacity_at_one) and the tick bridge bulkCapacityFromTicks_eq_bulkCapacity recover endpoints and the discrete-to-continuous match by unfolding this equation with the evaporation-fraction map $n/N$.
why it matters
This is leg (2) of the dynamical recipe that turns unitarity plus Schmidt balance into a triangular Page curve without postulating the shape. Downstream, capacity_sum_invariant and dynamical_page_curve_one_statement use it with radiation capacity so $\min(S_{BH}(1-t),S_{BH}t)$ peaks at $t=1/2$ and returns to zero. Tick forms (bulkCapacityFromTicks_*, bulkCapacityAtTick_eq) identify finite emitted recognition ticks with the same linear law. MasterTheorem handoff Track3TickCapacityEndpoint packages the fork: tick-induced transfer conserves total capacity and evaluates to the existing Schmidt min curve. Closes the structural gap left by PageCurveStructural's hand-drawn triangle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.