recognition_tick_capacity_transfer_prop
plain-language theorem explainer
Packages four equalities that turn discrete recognition-tick bookkeeping into the continuous Page curve: each emitted tick moves exactly S_BH/N of capacity from bulk to radiation, the sum stays S_BH, and the min-of-capacities ledger curve matches the unitarity Page curve at the tick fraction n/N. Gravity and QG master-theorem witnesses cite it as the dynamical transfer law. It is a pure Prop definition; the companion theorem discharges all four conjuncts from the tick capacity defs.
Claim. The recognition-tick capacity-transfer package is the conjunction of: (i) for every black-hole entropy $S_{BH}$ and tick budget $N>0$, each step $n\mapsto n+1$ raises radiation capacity by $S_{BH}/N$; (ii) when $n+1\le N$, the same step lowers bulk capacity by $S_{BH}/N$; (iii) for $n\le N$, bulk plus radiation capacity equals $S_{BH}$; (iv) for $n\le N$, the ledger-tick Page curve equals the continuous unitarity Page curve evaluated at evaporation fraction $n/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 capacities are linear: bulk $S_{BH}(1-t)$, radiation $S_{BH},t$. On a pure joint bulk$\otimes$radiation state, Schmidt purification forces equal reduced entropies bounded by $\min$ of the two capacities; saturating that bound yields the triangular Page curve peaking at $t=1/2$.
The discrete layer replaces $t$ by an emitted-tick count $n$ out of budget $N$. Evaporation fraction is $n/N$. Bulk capacity from ticks is $S_{BH}\cdot(N-n)/N$; radiation capacity is $S_{BH}\cdot n/N$. The ledger-tick Page curve is the min of those two. The continuous unitarity curve is the same min at a real fraction $t$. This definition packages the transfer, conservation, and discrete-to-continuous matching statements that make the tick model a faithful discretization of the dynamical recipe.
proof idea
No proof body: this is a Prop-valued definition, a four-way conjunction of universal statements over $S_{BH}$, $N$, and $n$. Each conjunct is written directly in terms of the tick capacity and Page-curve defs (radiation/bulk capacity from ticks, ledger-tick curve, unitarity curve, evaporation fraction). The companion theorem recognition_tick_capacity_transfer_prop_holds later discharges the package by refining into four goals and applying the elementary next-step and sum lemmas for those defs.
why it matters
This package is the dynamical content that Session 101 lacked: capacity transfer is no longer a kinematic ansatz but a tick-by-tick ledger law. Downstream, page_curve_derived_from_recognition_ticks_prop conjoins it with the Schmidt-balanced dynamical Page proposition for the QG master theorem. Nontrivial and operator Page-curve witnesses both store it as the first conjunct of page_curve_derived, and the noncircularity audit names it explicitly as the nontrivial D4 Page field (not True, not the master conclusion alone). It closes the discrete half of Track 3.C: conserved linear transfer under recognition ticks, matching the continuous unitarity curve at $n/N$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.