bulkCapacityFromTicks_next
plain-language theorem explainer
Each recognition tick inside a finite evaporation budget of N ticks removes exactly S_BH/N of bulk Schmidt capacity. Gravity Track 3.C and the MasterTheorem handoff cite this as the discrete bulk half of uniform capacity transfer. The proof reduces the tick form to the continuous linear bulk capacity and cancels by field arithmetic.
Claim. Fix black-hole entropy $S_{BH}\in\mathbb{R}$ and a positive tick budget $N\in\mathbb{N}$. For every tick index $n$ with $n+1\le N$, the bulk capacity after $n$ ticks minus the bulk capacity after $n+1$ ticks equals $S_{BH}/N$.
background
Module Gravity.PageCurveDynamical 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 moved from bulk to radiation. Continuous bulk capacity is the linear law $S_{BH}\cdot(1-t)$; radiation capacity is $S_{BH}\cdot t$. Unitary evolution from a pure bulk state keeps the joint bulk$\otimes$radiation state pure, so Schmidt forces equal subsystem entropies bounded by $\min$ of the two capacities; saturating that bound yields the Page triangle peaking at $t=1/2$.
The discrete side counts recognition ticks. With budget $N>0$, the evaporation fraction after $n$ ticks is the rational $n/N$ (while $n\le N$). Bulk capacity from ticks is that continuous bulk law evaluated at the tick-induced fraction. The RS tick $\tau_0=1$ is the fundamental time quantum; here $N$ is only a finite ledger budget, not an appeal to the eight-tick octave.
Upstream arithmetic supplies $n\le N$ from $n+1\le N$ via successor and transitivity of $\le$, so both neighboring tick indices stay inside the domain of the continuous identification lemmas.
proof idea
From $n+1\le N$ obtain $n\le N$ by le_trans with Nat.le_succ. Rewrite both sides via bulkCapacityFromTicks_eq_bulkCapacity, which identifies the tick form with continuous bulkCapacity at the tick-induced evaporation fraction. Unfold bulkCapacity and evaporationFractionFromTicks to expose the linear expressions $S_{BH}(1-n/N)$ and $S_{BH}(1-(n+1)/N)$. Cast $N\ne 0$ from $0<N$, then field_simp, normalize the successor cast $(n+1:\mathbb{R})=n+1$, and finish with ring. The difference collapses to the constant step $S_{BH}/N$.
why it matters
Uniform bulk decrement per tick is the bulk half of the recognition-tick capacity-transfer property: each emitted tick moves a fixed capacity quantum from bulk to radiation inside the budget. Downstream, recognition_tick_capacity_transfer_prop_holds packages this with the matching radiation increment, the sum invariant, and the curve identity. The MasterTheorem handoff consumes it inside track3_tick_capacity_endpoint_holds (Fork D endpoint) together with the radiation twin and the sum invariant, closing Track 3.C's bridge from discrete ledger ticks to the Session 112 min-of-capacities Page curve.
In the broader RS gravity story this is structural, not phenomenological: the triangular shape is forced by Schmidt purity plus linear capacity bookkeeping, with no free Page-time parameter. It does not itself invoke T5–T8 forcing, RCL, or the $\phi$-ladder mass formula; those sit upstream of the constants and ledger substrate this module assumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.