pageCurveFromLedgerTicks
plain-language theorem explainer
The ledger-tick Page curve is the pointwise minimum of remaining bulk entropy capacity and emitted radiation capacity, both linear in the fraction of recognition ticks already emitted. Anyone deriving black-hole radiation entropy from Schmidt-balanced ledger dynamics cites this as the discrete-time Page curve. The body is a one-line definition wrapping the two tick-induced capacities.
Claim. For black-hole entropy $S_{BH}\in\mathbb{R}$ and total recognition-tick count $N\in\mathbb{N}$, after $n$ emitted ticks the Page-curve value is $\min\bigl(S_{BH}\cdot(N-n)/N,\, S_{BH}\cdot n/N\bigr)$.
background
Gravity 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. Bulk capacity falls as $S_{BH}(1-t)$; radiation capacity rises as $S_{BH},t$. Purity of the joint bulk$\otimes$radiation state plus Schmidt's theorem force both reduced entropies to equal and to be bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$.
Here the continuous fraction is replaced by discrete recognition ticks: the fundamental RS time quantum $\tau_0=1$ (one tick). With total budget $N$ ticks and $n$ already emitted, bulk capacity is $S_{BH}\cdot(N-n)/N$ and radiation capacity is $S_{BH}\cdot n/N$. The Page value is their minimum, saturating the Schmidt bound under maximal entanglement.
proof idea
Pure definitional wrapper. The body is the real minimum of the two sibling capacities bulkCapacityFromTicks and radiationCapacityFromTicks, which themselves are the linear scalings $S_{BH}\cdot(N-n)/N$ and $S_{BH}\cdot n/N$. No lemmas or tactics are involved.
why it matters
This is the discrete-time Page curve that Track 3.C feeds into the master-theorem handoff. Track3TickCapacityEndpoint requires that finite emitted ticks induce bulk/radiation capacity transfer, conserve total capacity, and evaluate to the Schmidt min curve at the tick-induced evaporation fraction. The noncircularity audit d4_page_field_nondegenerate uses interior values of this curve to prove the Page field is non-vacuous (strict rise from the zero endpoint to a peak of height $S_{BH}/2$). Operator readout structures (OperatorPageEntropyReadout, canonicalOperatorPageEntropyReadout) demand that radiation entropy extracted from the operator process match this ledger-tick curve. Endpoint lemmas (pageCurveFromLedgerTicks_at_zero, _at_full, _at_page_fraction) and the bridge pageCurveAtTick_eq_unitarity_curve pin the discrete curve to the continuous unitarity ansatz. Framework-wise it realizes the dynamical recipe of Track 3.C: the triangular shape and half-evaporation peak are forced by min-of-two-monotone-bounds, not chosen by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.