tick_surjective
plain-language theorem explainer
Any reversible Page-tick operator on the bulk⊗radiation ledger is surjective: every joint state is hit by the forward tick. Gravity and Page-curve workers cite this when they need the tick map to cover the full carrier before applying capacity or entropy bounds. The proof is a one-line right-inverse witness from the structure's untick field.
Claim. Let $U$ be a reversible $\mathbb{C}$-linear tick on the finite bulk$\otimes$radiation ledger (with linear inverse satisfying both inverse laws). Then the forward tick map is surjective: for every joint state $\Psi$ there exists $\Phi$ with $U.{\rm tick}(\Phi)=\Psi$.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterized by $t\in[0,1]$; bulk capacity falls as $S_{BH}(1-t)$ and radiation capacity rises as $S_{BH}t$. Purity of the joint state plus Schmidt balance force radiation entropy to equal $\min$ of the two capacities, which is the Page triangle.
PageTickUnitary is the algebraic interface for one unitary step on that closed carrier: a $\mathbb{C}$-linear tick, a linear untick, and both composition identities. No inner-product preservation is required at this layer; only invertibility. The RS tick constant $\tau_0=1$ is the discrete time quantum elsewhere in the stack, but here "tick" means the ledger operator itself.
proof idea
Term-mode, two lines. Introduce an arbitrary joint state $\Psi$. Supply the preimage untick Ψ and discharge surjectivity by the structure field tick_untick, which states $\mathrm{tick}(\mathrm{untick},\Psi)=\Psi$. No further lemmas are needed; the right inverse is data of the structure.
why it matters
Surjectivity is the half of bijectivity needed so that every bulk–radiation configuration remains reachable under reversible Page evolution. The module's dynamical recipe assumes unitary evolution from a pure initial bulk state; this lemma records that the operator interface actually covers the full Hilbert space of the ledger. Downstream siblings (pageCurveFromUnitarity, capacity constructions, ledger-tick Page curve) sit on the same interface; even with no direct used_by edge yet, the result closes the elementary functional-analysis gap that a named inverse implies onto. It is pure algebra on the structure, not a new physical input, and does not itself force the Page peak or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.