schmidtCapacityBound_zero
plain-language theorem explainer
At the start of evaporation the Schmidt capacity bound on radiation entropy is identically zero. Anyone deriving the Page curve from an operator-level bulk-radiation process cites this initial boundary condition. The argument unfolds the capacity definition and applies the ledger-tick identity that zero emitted ticks force zero radiation entropy.
Claim. For any operator Page process $P$ on finite bulk and radiation type carriers, the Schmidt capacity bound of $P$ evaluated at tick $0$ equals $0$: there is no radiation entropy before evaporation begins.
background
Track 3.C builds an operator-derived Page entropy. An operator Page process packages a closed bulk-radiation ledger: a nonnegative black-hole entropy scale $S_{BH}$, a positive finite evaporation tick budget, and (upstream) a reversible linear tick operator on a finite bulk $\otimes$ radiation carrier. It is an interface: it supplies the unitary tick surface without assuming a microscopic Hamiltonian entropy readout.
The dynamical Page curve from ledger ticks is the triangular min-capacity that rises with emitted ticks and falls under unitarity once the radiation subsystem saturates. Upstream, the identity that no emitted ticks means zero radiation entropy states that this curve vanishes at tick $0$. The Schmidt capacity bound is the same triangular capacity, read off the process fields rather than supplied as a free readout field.
This module's goal is to derive the readout equality from the operator process (capacity bound, then Schmidt saturation implies Page equality), so master-theorem witnesses no longer depend on a field literally named as the Page-curve readout.
proof idea
One-line term proof. Unfold the Schmidt capacity bound (which is the ledger-tick Page curve evaluated on the process's $S_{BH}$ and total tick budget). Discharge the resulting goal by the upstream lemma that the ledger-tick Page curve at tick $0$ is zero, feeding nonnegativity of $S_{BH}$ and positivity of the tick budget from the process structure.
why it matters
This is the left boundary condition for operator-derived Page entropy in Gravity Track 3.C. Together with the matching full-evaporation bound (radiation entropy forced back to zero by information preservation), it pins the triangular capacity that Schmidt saturation must match.
The module status is structural theorem: zero sorry, zero RS-internal axiom. By defining capacity from the process and proving saturation implies the Page equality, the track supersedes the earlier field-based witness that carried readout equality as an assumption. Sibling results (saturation at zero, full, and peak; the canonical saturated process; the operator-derived Page-curve proposition) sit on this boundary identity.
In the broader Recognition frame this is gravity-side bookkeeping of reversible ledger ticks, not a new forcing-chain step (T5--T8). It makes the Page curve a derived capacity statement rather than an inserted readout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.