schmidtCapacityBound
plain-language theorem explainer
Defines the Schmidt capacity bound of an operator Page process at tick n as the triangular Page value min(remaining bulk capacity, emitted radiation capacity). Anyone proving operator-derived Page entropy or Schmidt saturation cites this bound as the ceiling on radiation entropy for a pure joint state. The body is a one-line alias of the ledger-tick Page curve on the process's black-hole entropy and total tick budget.
Claim. For an operator Page process $P$ on finite bulk and radiation carriers, with initial black-hole entropy $S_{\mathrm{BH}}\ge 0$ and positive total tick budget $N$, the Schmidt capacity bound at tick $n$ is $\min\bigl(C_{\mathrm{bulk}}(S_{\mathrm{BH}},N,n),\,C_{\mathrm{rad}}(S_{\mathrm{BH}},N,n)\bigr)$, i.e. the ledger-tick Page curve evaluated at the tick-induced evaporation fraction. It is the maximum radiation entropy consistent with Schmidt purification of a pure joint bulk-radiation state.
background
Gravity Track 3.C upgrades the dynamical Page curve from a supplied readout field to a quantity derived from an operator process. An operator Page process packages a closed bulk-radiation ledger, a nonnegative initial black-hole entropy $S_{\mathrm{BH}}$, a reversible linear tick operator, and a finite evaporation budget $N>0$. It deliberately stops short of fixing a microscopic Hamiltonian; it only supplies the carrier and unitary tick surface.
The ledger-tick Page curve is the pointwise minimum of remaining bulk capacity and emitted radiation capacity at the evaporation fraction induced by tick $n$. That triangular shape is the classical Page bound: radiation entropy cannot exceed either the entropy already emitted or the entropy still left in the bulk if the global state stays pure.
Schmidt purification supplies the information-theoretic reading: for a pure joint state, the von Neumann entropy of either factor is bounded by that capacity minimum. The present definition simply names that bound on a concrete operator process.
proof idea
Definitional one-liner. Unfolding replaces the bound by pageCurveFromLedgerTicks applied to the process fields $S_{\mathrm{BH}}$ and totalTicks at tick $n$. No extra algebra; all nontrivial identities live in the upstream ledger-tick lemmas (zero, full evaporation, half-Page peak).
why it matters
This is step 1 of the module's three-step derivation: define the capacity bound from the operator process, prove that Schmidt saturation (entropy equals the bound) forces the Page readout equality, then build a master-theorem witness that no longer depends on a supplied readout_eq_page_curve field.
Downstream, the bound is the saturation target in SchmidtSaturatedOperatorProcess, and the elementary evaluations at $n=0$, full evaporation, and the half-Page fraction are proved directly from it. The canonical single-tick saturated process uses the same bound to make the Page curve identically zero, so saturation reduces to a two-point case split. In the broader RS gravity track this closes the structural gap between unitary tick evolution and the triangular Page curve without importing an external entropy ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.