stateAfterOperatorTicks_zero
plain-language theorem explainer
Zero applications of a reversible Page tick leave any bulk-radiation joint state unchanged. Anyone building the dynamical Page process from iterated unitary ticks cites this as the iterator base case. The proof is pure definitional reflexivity from the recursive clause at n = 0.
Claim. Let $U$ be a reversible $\mathbb{C}$-linear tick on the closed bulk$\otimes$radiation carrier, and let $\Psi$ be any joint state on that carrier. Then the state obtained after $0$ ticks equals $\Psi$.
background
Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterized by a tick count; bulk capacity falls and radiation capacity rises, while unitary evolution keeps the joint bulk$\otimes$radiation state pure, so radiation entropy saturates $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$.
The closed carrier is the tensor product bulk ledger $\otimes$ Hawking-radiation ledger. A Page tick unitary records a $\mathbb{C}$-linear tick map with a linear inverse and both inverse laws (algebraic unitarity; metric preservation is deferred).
The iterator stateAfterOperatorTicks folds that tick: at zero steps it returns the input state; at successor steps it applies the tick to the previous iterate. This lemma is exactly the zero clause of that recursion.
proof idea
One-line definitional proof by rfl. The recursive definition of the iterator has base clause | 0, Ψ => Ψ, so equality to the input state is judgmental and needs no further lemmas.
why it matters
Without a clean zero-tick identity, induction and simp normalization over iterated Page ticks cannot start. The module's dynamical recipe builds bulk and radiation capacities from tick counts and recovers the triangular Page curve as $\min$ of those capacities under Schmidt balance; this simp lemma is the base of that operator-level iteration.
It sits under Gravity Track 3.C (structural theorem, zero sorry). Downstream used-by edges are empty in the graph snapshot, but sibling results (pageCurveFromLedgerTicks, capacity-from-ticks lemmas) rely on the same iterator. Framework link: unitary closed-system evolution of the joint ledger, the substrate step that forces the Page peak at half-evaporation rather than inserting it by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.