schmidtCapacityBound_full
plain-language theorem explainer
At full evaporation the Schmidt capacity bound of an operator Page process vanishes: radiation entropy is forced back to zero by unitarity. Anyone deriving the triangular Page curve from a closed bulk-radiation ledger cites this endpoint. The proof unfolds the capacity definition and applies the ledger-tick identity at emitted-tick count equal to the total budget.
Claim. Let $P$ be an operator Page process on finite bulk and radiation carriers, with initial black-hole entropy $S_{\mathrm{BH}}\ge 0$ and total evaporation tick budget $N>0$. The Schmidt capacity bound of $P$ at tick $N$ equals zero: $\min(\text{bulk capacity},\text{radiation capacity})$ at full evaporation fraction is $0$.
background
Track 3.C builds an operator-level Page process: a closed bulk-radiation ledger, an initial state, a reversible linear tick operator, and a finite evaporation budget $N$. The structure carries initial entropy $S_{\mathrm{BH}}\ge 0$ and $N>0$ without presupposing a microscopic Hamiltonian.
The Schmidt capacity bound at tick $n$ is the triangular Page curve evaluated on the ledger: $\mathrm{pageCurveFromLedgerTicks}(S_{\mathrm{BH}},N,n)$, i.e. the maximum entropy consistent with Schmidt purification of a pure joint state (min of bulk and radiation capacities at the tick-induced evaporation fraction).
Upstream, pageCurveFromLedgerTicks_at_full already states that at full emitted-tick count the bulk capacity vanishes and radiation entropy returns to zero. Entropy in the foundation layer is total defect, so zero defect is the minimum-entropy pure state.
proof idea
One-line term proof after unfolding. Unfold the Schmidt capacity bound definition, which is exactly pageCurveFromLedgerTicks on $P$'s initial entropy and total tick budget. Then apply pageCurveFromLedgerTicks_at_full to $P.S_{\mathrm{BH}}$, $P.\mathrm{totalTicks}$, using nonnegativity of $S_{\mathrm{BH}}$ and positivity of the tick budget. No further algebraic work.
why it matters
This is the full-evaporation endpoint of the operator-derived Page curve in Gravity Track 3.C. The module's goal is to derive the readout equality from the operator process rather than supply it as a structure field: define the Schmidt capacity bound, prove saturation implies the Page curve, and build a witness that does not depend on a field named readout_eq_page_curve.
Together with the zero-tick and Page-fraction siblings, it pins the triangular shape (start at 0, peak at half entropy, return to 0). That return-to-zero is the information-preservation statement: a pure joint state under unitary ticks ends pure on the radiation side when the bulk is fully evaporated. No downstream dependents are recorded yet; the declaration feeds the saturated-process equalities in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.