bulkCapacityAtTick_eq
plain-language theorem explainer
At any admissible tick of an operator Page process, bulk entropy capacity computed from remaining ticks equals the continuous linear bulk capacity at that tick's evaporation fraction. Gravity and information theorists working the discrete-to-continuous Page bridge cite it. The proof is a one-line wrapper of the general tick-capacity identity, feeding the process's total-tick positivity and the bound n ≤ totalTicks.
Claim. Let $P$ be an operator Page process with initial bulk entropy $S_{\mathrm{BH}}$ and total tick budget $N>0$. For every tick index $n\le N$, the bulk capacity induced by remaining ticks equals the continuous bulk capacity at the process evaporation fraction: $S_{\mathrm{BH}}\cdot(N-n)/N = S_{\mathrm{BH}}\cdot(1-t_n)$, where $t_n=n/N$.
background
Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterized by a fraction $t\in[0,1]$: bulk Hilbert-space entropy capacity falls linearly as $S_{\mathrm{BH}}(1-t)$, while radiation capacity rises as $S_{\mathrm{BH}},t$. Unitary evolution from a pure bulk state keeps the joint bulk⊗radiation state pure, so Schmidt forces equal reduced entropies bounded by $\min$ of the two capacities; that min is the Page curve.
An operator Page process packages a closed bulk-radiation ledger, initial state, reversible tick operator, and finite tick budget $N$, with initial bulk entropy $S_{\mathrm{BH}}\ge 0$. Discrete capacities are read from remaining or emitted ticks: bulk capacity from ticks is $S_{\mathrm{BH}}\cdot(N-n)/N$. The process evaporation fraction at tick $n$ is the same tick-induced fraction $n/N$ used in the capacity-transfer layer.
Upstream, the general identity already equates tick bulk capacity with continuous bulk capacity at the tick-induced fraction, under $0<N$ and $n\le N$. This declaration specializes that bridge to the fields of an operator process.
proof idea
One-line wrapper. Apply bulkCapacityFromTicks_eq_bulkCapacity to $S_{\mathrm{BH}}$, total tick count $N$, and index $n$, discharging the hypotheses with the process field totalTicks_pos ($0<N$) and the given bound $n\le N$. Unfolding is already done in the upstream lemma; no further algebra is needed here.
why it matters
This is the operator-level specialization of the first discrete bridge from emitted ledger ticks to the continuous Page-curve parameter. The module's dynamical recipe needs bulk capacity at each tick of a unitary tick process to match the linear continuum formula so that min(bulk, radiation) still yields the triangle with forced peak at half-evaporation.
It sits in Gravity Track 3.C (structural theorem, zero sorry), which upgrades Session 101's kinematic ansatz to a derivation from Schmidt purification on the bulk⊗radiation ledger. No downstream dependents are recorded yet; the natural consumers are operator-level Page-curve statements that read capacity along OperatorPageProcess trajectories rather than bare real parameters. Framework-wise it is ledger bookkeeping for black-hole evaporation entropy, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.