stateAtTick_succ
plain-language theorem explainer
After each discrete tick, the bulk-radiation state of an operator-level Page process is exactly the image of the previous state under the process's reversible linear tick map. Anyone citing the dynamical Page-curve interface or the operator-process certificate needs this one-step evolution law. The proof is definitional reflexivity: the successor clause is how the iterated state is defined.
Claim. Let $P$ be an operator-level Page process on finite bulk and radiation labels, with reversible linear tick map $U$ and initial joint state $\psi_0$. Write $\psi_n$ for the state after $n$ ticks. Then for every $n\in\mathbb{N}$, $\psi_{n+1}=U(\psi_n)$.
background
Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating a piecewise-linear ansatz. Evaporation is parameterized by a fraction $t\in[0,1]$ of total entropy moved from bulk to radiation; bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ and radiation capacity rises as $S_{\mathrm{BH}}t$. Unitary evolution from a pure initial bulk state keeps the joint bulk$\otimes$radiation state pure, so Schmidt forces equal subsystem entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$. Under maximal entanglement that bound saturates and yields the triangular curve peaking at $t=1/2$.
An operator-level Page process packages the closed bulk-radiation ledger, a nonnegative black-hole entropy scale $S_{\mathrm{BH}}$, a positive finite tick budget, a reversible $\mathbb{C}$-linear tick operator on the joint carrier, and an initial joint state. The fundamental RS time quantum is one tick ($\tau_0=1$). The state after $n$ ticks is the $n$-fold iterate of that tick map on the initial state; this lemma records the successor step of that iteration.
proof idea
Term-mode proof by rfl. The successor identity is definitional: stateAtTick (n+1) is defined to be the tick operator applied to stateAtTick n, so the equality holds by unfolding. No external lemmas are invoked.
why it matters
This is the discrete evolution law that makes the operator Page process dynamical rather than a static ledger snapshot. Downstream, pageCurveOperatorProcessCert wires it in as state_evolves_by_tick, and operator_page_process_interface_one_statement packages it into the one-statement interface: explicit bulk-radiation carrier, reversible linear Page tick, iterated states evolving by that tick, and an entropy readout linking the operator process to the ledger-tick Page curve.
In the broader RS gravity track this sits under the structural closure of Track 3.C (triangular Page curve from unitarity and Schmidt balance, not a hand-drawn ansatz). It does not yet close the open gap named in the interface theorem: deriving the entropy readout from a specific microscopic Hamiltonian or recognition update. The eight-tick octave and forcing chain are ambient RS time structure; this lemma only needs the single-tick successor on the joint carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.