bulkCapacityFromTicks_eq_bulkCapacity
plain-language theorem explainer
Tick-counted bulk entropy capacity equals the continuous linear bulk capacity evaluated at the discrete evaporation fraction n/N. Anyone bridging ledger-tick evaporation to the Schmidt Page curve cites this identity. The proof unfolds the three definitions and finishes by field simplification after a natural-number cast.
Claim. Let $S_{BH}\in\mathbb{R}$ be the initial black-hole entropy capacity, let $N>0$ be the total number of recognition ticks in the evaporation budget, and let $n\le N$ be the number already emitted. Then the bulk capacity induced by the remaining ticks equals $S_{BH}\cdot(1-t)$ at the tick-induced evaporation fraction $t=n/N$.
background
Module Gravity.PageCurveDynamical (Track 3.C) derives the triangular Page curve from Schmidt purification on bulk ⊗ radiation, rather than postulating it. Evaporation is parameterized by a fraction $t\in[0,1]$: bulk Hilbert-space entropy capacity falls linearly as $S_{BH}(1-t)$, while radiation capacity rises as $S_{BH},t$. The joint pure state forces radiation entropy to saturate $\min$ of those two bounds, which is the triangle peaking at $t=1/2$.
The continuous bulk capacity is the linear map $S_{BH}\mapsto S_{BH}(1-t)$. The discrete counterpart counts remaining recognition ticks: after $n$ of $N$ ticks have been emitted, bulk capacity is $S_{BH}\cdot(N-n)/N$. The companion evaporation fraction is the ratio of emitted ticks to the budget. This theorem is the algebraic identification of those two bulk expressions.
proof idea
Tactic proof by definitional reduction. Unfold the three defs (tick bulk capacity, continuous bulk capacity, and tick evaporation fraction). From $N>0$ obtain $(N:\mathbb{R})\neq 0$ by casting. Rewrite the natural subtraction under the cast via Nat.cast_sub (using $n\le N$). A single congr 1 reduces the claim to equality of the scalar factors $(N-n)/N$ and $1-n/N$, which field_simp discharges.
why it matters
Doc-comment calls this the first discrete bridge from emitted ledger ticks to the continuous Page-curve parameter. Downstream it is the bulk half of the main bridge theorem equating the ledger-tick Page curve to the Schmidt-capacity curve at the tick-induced fraction. It also feeds the tick capacity sum invariant (conservation of $S_{BH}$ under the discrete split), the one-tick decrement identity for bulk capacity, the operator-process specialization at a concrete tick index, and the Track 3 tick-capacity endpoint package consumed by MasterTheoremHandoffIntegration.
In the broader RS gravity track this closes the discrete-to-continuous handoff for bulk capacity inside the dynamical Page-curve derivation, so the triangular shape forced by Schmidt balance can be read off a finite recognition-tick ledger rather than only a continuous ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.