radiationCapacityAtTick_eq
plain-language theorem explainer
Radiation entropy capacity computed from discrete evaporation ticks equals the continuous radiation capacity evaluated at the process's tick-induced evaporation fraction. Anyone wiring the operator Page process to the capacity-transfer layer cites this bridge. The proof is pure definitional equality (rfl).
Claim. For any operator-level Page process $P$ (closed bulk-radiation ledger with initial black-hole entropy $S_{BH}$, finite tick budget $N$, and unitary tick) and any tick index $n\in\mathbb{N}$, the tick-induced radiation capacity $S_{BH}\cdot(n/N)$ equals the continuous radiation capacity $S_{BH}\cdot t$ at the evaporation fraction $t$ that $P$ assigns to tick $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]$ of total entropy transferred from bulk to radiation. Radiation Hilbert-space capacity grows linearly: $\mathrm{radiationCapacity}(S_{BH},t)=S_{BH}\cdot t$, from $0$ at $t=0$ to $S_{BH}$ at full evaporation.
The discrete layer uses the same linear law on tick counts: $\mathrm{radiationCapacityFromTicks}(S_{BH},N,n)=S_{BH}\cdot(n/N)$. An OperatorPageProcess packages $S_{BH}$, a positive finite tick budget, a unitary tick operator on the bulk$\otimes$radiation ledger, and an initial state, without committing to a microscopic Hamiltonian for the entropy readout.
The process's evaporation fraction at tick $n$ is exactly the capacity-transfer fraction $n/N$. This theorem records that the two radiation-capacity presentations agree on that fraction.
proof idea
One-line definitional proof: rfl. Unfolding evaporationFractionAtTick (which is evaporationFractionFromTicks on P.totalTicks), radiationCapacityFromTicks, and radiationCapacity yields identical terms $S_{BH}\cdot(n/N)$ on both sides, so the equality is by reflexivity of definitional equality.
why it matters
Closes the interface between the continuous capacity-transfer recipe (linear radiation growth that, with bulk shrinkage and Schmidt purity, forces the triangular Page curve as $\min$ of the two capacities) and the operator-level process that carries an explicit bulk$\otimes$radiation ledger and unitary tick. Without this identification, tick-indexed radiation capacity and fraction-indexed radiation capacity would be parallel APIs.
The module status is structural theorem (0 sorry): the Page curve is no longer a kinematic ansatz from Session 101 but emerges from unitarity plus Schmidt balance. This lemma is a small but necessary coherence step in that derivation chain. No downstream dependents are recorded yet; sibling results such as pageCurveFromLedgerTicks and the capacity-sum invariant sit in the same layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.