stateAfterOperatorTicks
plain-language theorem explainer
Recursive discrete evolution of a bulk-radiation joint state under a reversible Page tick. Gravity and Page-curve workers cite it as the operator-level clock for evaporation. Defined by recursion: identity at zero ticks, then one more application of the unitary tick.
Claim. Given a reversible $\mathbb{C}$-linear tick $U$ on the closed bulk$\otimes$radiation carrier, the state after $n$ operator ticks of an initial joint state $\Psi$ is $\Psi$ if $n=0$, and equals $U$ applied to the state after $n$ ticks if the step is $n\mapsto n+1$.
background
Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. The carrier is the closed bulk-radiation ledger: bulk ledger tensor Hawking-radiation ledger over $\mathbb{C}$. A Page tick unitary packages a linear tick and linear inverse with both inverse laws on that carrier; metric unitarity can be refined later without changing the interface.
Evaporation is parameterized by discrete ticks. Capacities move linearly with the evaporated fraction: bulk capacity falls as $S_{BH}(1-t)$, radiation capacity rises as $S_{BH},t$. Purity of the joint state plus Schmidt balance force radiation entropy to saturate $\min$ of the two capacities, which is the triangle.
The RS tick is the fundamental time quantum ($\tau_0=1$ in native units). Here the tick is the algebraic Page step on the joint ledger, not the continuum Hamiltonian exponential.
proof idea
Definition by structural recursion on $\mathbb{N}$, not a proved theorem. Base case returns the input state unchanged. Successor case applies the tick map of the given Page tick unitary to the recursively computed prior state. The companion simp lemmas are definitional equalities (rfl) for the zero and successor clauses.
why it matters
This is the discrete dynamical skeleton for operator-level Page evolution. stateAtTick is the thin wrapper that feeds a process's unitary tick and initial state through this iterator. Downstream entropy theorems in PageCurveOperatorEntropy evaluate radiation entropy on stateAfterOperatorTicks ... n ... and identify it with the ledger Page curve under Schmidt saturation: equality to the curve, return to zero at full evaporation, and peak $S_{BH}/2$ at half evaporation.
It closes the gap left by the kinematic Session-101 ansatz: the triangle is read off unitary tick dynamics on a pure joint state, not drawn by hand. Landmark contact is the eight-tick octave only at the level of the ambient RS clock; the Page process uses its own total-tick horizon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.