stateAtTick
plain-language theorem explainer
After n discrete Page ticks of an operator-level evaporation process, the closed bulk–radiation joint state is the n-fold iterate of the process’s unitary tick on its initial ledger state. Anyone citing the Track 3.C operator Page interface, the one-statement process certificate, or the MasterTheorem handoff endpoint uses this readout. The body is a one-line wrapper around the existing tick-iteration map.
Claim. Let $P$ be an operator-level Page process on finite bulk and radiation labels (black-hole entropy bound $S_{BH}\ge 0$, positive total tick budget, reversible $\mathbb{C}$-linear tick, and initial joint state). For each $n\in\mathbb{N}$, the state at tick $n$ is the closed bulk–radiation ledger obtained by applying $P$'s unitary tick operator $n$ times to $P$'s initial state.
background
Module Gravity.PageCurveDynamical (Track 3.C) derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterised by a tick fraction $t\in[0,1]$; bulk capacity falls as $S_{BH}(1-t)$ and radiation capacity rises as $S_{BH},t$. Unitary evolution keeps the joint bulk$\otimes$radiation state pure, so Schmidt forces equal reduced entropies bounded by $\min$ of the two capacities; that $\min$ is the Page triangle.
BulkRadiationLedger is the Lean carrier BulkLedger $\otimes_{\mathbb{C}}$ HawkingRadiationLedger. OperatorPageProcess packages $S_{BH}$, a positive finite tick budget, a reversible linear Page tick, and an initial joint state, as an interface without fixing a microscopic Hamiltonian. Upstream stateAfterOperatorTicks iterates a PageTickUnitary by recursion: identity at $0$, then one tick application at each successor.
proof idea
Definitional one-line wrapper. It feeds the process’s unitary tick and initial joint state into stateAfterOperatorTicks and returns the $n$-step iterate. No extra algebra: the recursion and inverse laws live in the tick iterator and the unitary tick structure. Downstream simp lemmas stateAtTick_zero and stateAtTick_succ are immediate rfl unfoldings of this definition.
why it matters
Gives the dynamical state trajectory that the operator Page interface talks about. Downstream, stateAtTick_zero and stateAtTick_succ record the base and step laws; operator_page_process_interface_one_statement and PageCurveOperatorProcessCert package carrier nonemptiness, unitary tick, entropy readout, and the successor law $P.\mathrm{stateAtTick}(n+1)=U(P.\mathrm{stateAtTick},n)$; MasterTheorem handoff Track3OperatorProcessEndpoint reuses the same bundle as the Agent D structural endpoint.
In the framework this is the operator surface under the kinematic capacity layer that yields $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$. It does not close microscopic entropy-from-Hamiltonian derivation; the module doc and the one-statement theorem both flag that readout-from-Hamiltonian gap as still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.