radiationCapacityFromTicks
plain-language theorem explainer
Radiation entropy capacity after n of N recognition ticks during black-hole evaporation: S_BH times the emitted fraction n/N. Anyone deriving the discrete ledger-tick Page curve or capacity-transfer identities cites this. It is a pure arithmetic definition matching the continuous linear radiation capacity at the tick-induced evaporation fraction.
Claim. For black-hole entropy $S_{\mathrm{BH}}\in\mathbb{R}$ and natural numbers $N$ (total evaporation ticks) and $n$ (emitted ticks), the radiation entropy capacity is $S_{\mathrm{BH}}\cdot 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 parameterized by a fraction of total entropy transferred from bulk to radiation. In the continuous picture, radiation capacity grows as $S_{\mathrm{BH}}\cdot t$ while bulk capacity shrinks as $S_{\mathrm{BH}}\cdot(1-t)$.
Here time is discrete: $N$ is the total recognition-tick budget for full evaporation and $n$ is the number already emitted. The fundamental RS time quantum is one tick ($\tau_0=1$). The continuous evaporation fraction is then the ratio $n/N$, so this definition is the tick-native form of linear radiation capacity.
Under unitary evolution from a pure initial bulk state, the joint bulk$\otimes$radiation state stays pure. Schmidt's theorem forces equal reduced entropies, each bounded by the minimum of the two capacities; saturating that bound yields the Page curve.
proof idea
Definition only: the body is the product of $S_{\mathrm{BH}}$ with the real ratio $n/N$. No lemmas or tactics. Downstream equalities such as equality to continuous radiationCapacity at the tick-induced fraction are definitional (rfl) once the evaporation fraction is $n/N$.
why it matters
This is the radiation half of the discrete capacity pair that builds the ledger-tick Page curve: pageCurveFromLedgerTicks takes the min of bulk and radiation capacities from ticks. It feeds the sum invariant (bulk plus radiation capacity equals $S_{\mathrm{BH}}$ at every tick), the one-step increment theorem (each tick adds $S_{\mathrm{BH}}/N$), and the operator-process form radiationCapacityAtTick_eq.
Downstream, MasterTheorem handoff Track3TickCapacityEndpoint packages the claim that finite emitted recognition ticks induce bulk/radiation capacity transfer, conserve total capacity, and evaluate to the Schmidt min Page curve at the tick-induced fraction. That closes Track 3.C: the triangular shape (peak at half evaporation, return to zero) emerges from ledger ticks plus purity, not from a kinematic ansatz.
Framework link: recognition ticks are the RS time quantum; the eight-tick octave is the deeper period, but here $N$ is the evaporation budget in ticks, not forced to 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.