bulkCapacityFromTicks
plain-language theorem explainer
Bulk entropy capacity after n of N recognition ticks equals initial black-hole entropy times the remaining-tick fraction (N-n)/N. Gravity Track 3.C cites it as the discrete bulk side of the ledger-tick Page curve. The body is a one-line arithmetic definition, not a derived identity.
Claim. Given initial black-hole entropy $S_{BH}$ and a finite evaporation budget of $N$ recognition ticks, the bulk entropy capacity after $n$ emitted ticks is $S_{BH}\cdot(N-n)/N$.
background
Module Gravity.PageCurveDynamical (Track 3.C) derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterised by a continuous fraction $t\in[0,1]$, with bulk capacity $S_{BH}(1-t)$ and radiation capacity $S_{BH},t$. Unitary evolution from a pure bulk state keeps the joint bulk$\otimes$radiation state pure, so Schmidt forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$.
This definition is the discrete counterpart: $N$ is the total recognition-tick budget and $n$ the number already emitted. Remaining bulk capacity is the linear share of $S_{BH}$ still carried by the unemitted ticks. Sibling radiationCapacityFromTicks grows as $S_{BH},n/N$; their minimum is the ledger-tick Page curve.
Upstream entropy names in Foundation, HorizonLedger, and Thermodynamics fix the ambient meaning of entropy (defect total, log microstate count, or Boltzmann $S=k\beta\langle E\rangle+k\ln Z$) but are not invoked in the body; the argument here is pure capacity bookkeeping.
proof idea
Definitional one-liner: cast the natural-number remainder $N-n$ and the budget $N$ to reals, form the ratio, and scale by $S_{BH}$. No lemmas, tactics, or side conditions appear in the body; positivity and $n\le N$ are imposed only by downstream theorems that relate this quantity to continuous bulkCapacity.
why it matters
This is the discrete bulk leg of the dynamical Page-curve recipe. Downstream pageCurveFromLedgerTicks takes $\min$ of this quantity and radiationCapacityFromTicks, recovering the triangular curve at tick resolution. bulkCapacityFromTicks_eq_bulkCapacity proves equality with continuous bulkCapacity at the tick-induced evaporation fraction, the first bridge from emitted ledger ticks to the continuous parameter $t$. bulkCapacityFromTicks_next shows each tick removes the same capacity quantum $S_{BH}/N$.
Track3TickCapacityEndpoint (MasterTheorem handoff, Fork D) packages the pair of tick-capacity identities, total-capacity conservation, and evaluation of the Schmidt $\min$ curve at the tick fraction. Capacity sum invariants (tick_capacity_sum_invariant, capacityAtTick_sum_invariant) use it to keep bulk plus radiation equal to $S_{BH}$. In the RS gravity track this closes the structural claim that the Page peak at half-evaporation is forced by finite recognition-tick transfer, not chosen by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.