capacity_sum_invariant
plain-language theorem explainer
Bulk and radiation Hilbert-space capacities always sum to the initial black-hole entropy at every evaporation fraction. Anyone citing the dynamical Page curve, the capacity certificate, or the discrete-tick form needs this conservation identity. The proof unfolds the two linear capacity definitions and cancels by ring arithmetic.
Claim. For all real $S_{\mathrm{BH}}$ and $t$, the bulk capacity $S_{\mathrm{BH}}(1-t)$ plus the radiation capacity $S_{\mathrm{BH}}\, t$ equals $S_{\mathrm{BH}}$.
background
This module derives the triangular Page curve from Schmidt purification on a pure joint bulk ⊗ radiation state, rather than postulating the triangle by hand. Evaporation is parameterized by a real fraction $t \in [0,1]$: $t=0$ is the initial black hole and $t=1$ is full evaporation.
Bulk capacity shrinks linearly as $S_{\mathrm{BH}}(1-t)$; radiation capacity grows as $S_{\mathrm{BH}}, t$. These are the log-dimension proxies for the two factors of the joint Hilbert space. Unitary evolution from a pure initial bulk state keeps the joint state pure, so Schmidt's theorem equates the reduced entropies and bounds each by the minimum of the two capacities.
The capacity-sum identity is the conservation law behind that picture: Hilbert-space capacity is only transferred, never created or destroyed, under the linear bulk-to-radiation handoff.
proof idea
One-line algebraic proof. Unfold the definitions of bulk capacity and radiation capacity to $S_{\mathrm{BH}}(1-t)$ and $S_{\mathrm{BH}}, t$, then apply ring to obtain $S_{\mathrm{BH}}(1-t)+S_{\mathrm{BH}}, t=S_{\mathrm{BH}}$. No external lemmas are required.
why it matters
This is the conservation hinge of Gravity Track 3.C. The one-statement dynamical Page curve theorem packages it as the second conjunct: capacities always sum to $S_{\mathrm{BH}}$, while the Page curve itself is the min of the two. The dynamical certificate records the same fact as its capacity_invariant field, so every certified consumer inherits the identity.
The discrete-tick variant reduces to this theorem after rewriting tick capacities into the continuous linear forms via the evaporation-fraction map. Without the sum invariant, the peak value $S_{\mathrm{BH}}/2$ at Page time $t=1/2$ and the return to zero at full evaporation would not be forced by the min construction alone.
In the broader Recognition gravity track this closes the structural gap left by the earlier kinematic Page-curve ansatz: capacity conservation is now a proved algebraic fact under linear transfer, not an extra modeling assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.