stateAfterOperatorTicks_succ
plain-language theorem explainer
Unfolding rule for the iterated unitary Page tick: the bulk–radiation ledger after n+1 ticks equals one more tick applied to the state after n ticks. Anyone simplifying discrete evaporation dynamics on the closed ledger will cite it. The proof is pure definitional equality (rfl), so it is a simp lemma rather than an analytic argument.
Claim. Let $U$ be a reversible $\mathbb{C}$-linear tick operator on the closed bulk–radiation ledger $H_{\mathrm{bulk}}\otimes H_{\mathrm{rad}}$, and let $\Psi$ be an initial ledger state. For every $n\in\mathbb{N}$, the state after $n+1$ ticks equals $U$ applied once to the state after $n$ ticks.
background
Track 3.C derives the triangular Page curve from Schmidt-balanced dynamics on a pure joint state, rather than postulating a piecewise-linear ansatz. Evaporation is parameterized by a tick budget; bulk capacity falls linearly and radiation capacity rises linearly, and unitarity plus Schmidt force the radiation entropy to track $\min$ of the two capacities.
The carrier is the closed bulk–radiation ledger BulkLedger β ⊗[ℂ] HawkingRadiationLedger ρ. A PageTickUnitary packages a linear tick and its linear inverse with both inverse laws; it is the algebraic unitary interface for one discrete Page step, without yet asserting metric inner-product preservation or a microscopic Hamiltonian entropy readout.
stateAfterOperatorTicks is the natural iteration of that tick from an initial ledger state. This lemma is the successor clause of that iteration, matching the RS tick quantum as the discrete time step of the process.
proof idea
Term-mode proof by rfl. The successor equation is definitionally identical to the recursive clause of the iterator that applies U.tick once more, so no lemmas are invoked and no rewriting beyond the definition is required. Marked @[simp] so tactics unfold n+1 ticks automatically.
why it matters
Gives Track 3.C a clean discrete-time surface for the operator-level Page process: closed ledger, initial state, reversible linear tick, finite evaporation budget. Together with the capacity functions and pageCurveFromLedgerTicks / pageCurveFromUnitarity siblings, it lets the triangular curve emerge as $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$ under Schmidt purity, instead of being drawn by hand as in Session 101.
No downstream theorems currently depend on it (used_by is empty), so it is infrastructure for the dynamical recipe rather than a cited parent result. It does not itself touch T5–T8 or the RCL; its role is local to Gravity Track 3.C’s unitary tick interface and the structural closure of the Page curve module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.