stateAtTick_zero
plain-language theorem explainer
After zero Page ticks the closed bulk-radiation ledger equals the process initial state. Anyone setting up the dynamical Page-curve iteration uses this as the base case of the tick map. The equality is definitional: zero applications of the unitary tick leave the ledger unchanged, so the proof is reflexivity.
Claim. For any operator-level Page process $P$ on bulk and radiation factors, the closed bulk-radiation ledger after $0$ ticks equals the initial state of $P$.
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 discrete tick budget on a closed bulk ⊗ radiation ledger; radiation entropy is forced to equal $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$ under purity and maximal Schmidt balance.
An OperatorPageProcess packages black-hole entropy $S_{BH}\ge 0$, a positive total tick count, a reversible linear tick operator, and an initial bulk-radiation ledger. It is an interface: it supplies a unitary tick surface without claiming a microscopic Hamiltonian entropy readout.
The state after $n$ ticks is defined by iterating that unitary tick on the initial ledger. The $n=0$ case is the natural base of that iteration.
proof idea
One-line definitional proof. The state-after-$n$-ticks map is the $n$-fold iterate of the unitary tick starting from the initial ledger; at $n=0$ the iterate is the identity on the initial state, so the equality holds by rfl. Marked @[simp] for automatic base-case reduction.
why it matters
Gives the clean $t=0$ anchor for the dynamical Page process: before any Hawking emission the ledger is still the initial pure bulk state. Downstream capacity and Page-curve identities in this module (bulk/radiation capacity at zero, capacity-sum invariance, page curve from unitarity and from ledger ticks) rely on a well-defined tick orbit; this simp fact discharges the zero-tick case without ceremony.
In the module recipe, $t=0$ is the unevaporated black hole and radiation capacity starts at zero. The theorem does not itself produce the triangular curve; it only fixes the initial point of the unitary tick dynamics from which that curve is later read off via Schmidt balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.