PageTickUnitary
plain-language theorem explainer
Algebraic interface for a reversible complex-linear tick on the closed bulk⊗radiation ledger: a linear map and its two-sided linear inverse. Gravity Track 3.C cites it as the unitary Page-tick surface under Schmidt-balanced ledger dynamics. As a structure it only packages the inverse laws; no metric unitarity is proved here.
Claim. For finite index types $\beta$ and $\rho$, a Page tick unitary is a pair of $\mathbb{C}$-linear endomorphisms $U,U^{-1}$ of the bulk–radiation carrier $\mathrm{BulkLedger}(\beta)\otimes_{\mathbb{C}}\mathrm{HawkingRadiation}(\rho)$ such that $U^{-1}\circ U=\mathrm{id}$ and $U\circ U^{-1}=\mathrm{id}$ on every joint state.
background
Track 3.C derives the triangular Page curve from Schmidt-balanced dynamics on a pure joint bulk⊗radiation state, rather than postulating a piecewise-linear ansatz. Evaporation is parameterized by a fraction $t\in[0,1]$; bulk capacity falls as $S_{BH}(1-t)$ and radiation capacity rises as $S_{BH},t$. Purity plus Schmidt forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$, and maximal entanglement saturates that bound, yielding the triangle peaking at $t=1/2$.
The closed carrier is the tensor product of two macroscopic Signal8 ledgers: remaining black-hole degrees of freedom and emitted Hawking modes. The RS tick is the fundamental time quantum ($\tau_0=1$), so discrete operator evolution is naturally indexed by ticks. This structure records only algebraic reversibility of one such tick on that carrier.
proof idea
Definitional structure, not a proved theorem. Fields are a $\mathbb{C}$-linear tick, a $\mathbb{C}$-linear untick, and the two inverse identities. Inhabitation is witnessed downstream by the identity maps (LinearMap.id for both directions with rfl inverse laws). No tactics discharge nontrivial goals at this declaration.
why it matters
Supplies the unitary tick surface demanded by the operator-level Page process. Downstream, OperatorPageProcess packages an initial joint state, this tick, and a finite evaporation budget; iterated evolution is stateAtTick (n+1) = unitaryTick.tick (stateAtTick n). The one-statement interface theorem and PageCurveOperatorProcessCert assert nonemptiness of this type alongside the bulk–radiation carrier and entropy readout. Master-theorem handoff (Track3OperatorProcessEndpoint) lists the same bundle as the Agent D structural endpoint.
It advances Session 101 kinematics toward dynamics: unitarity of the joint evolution is the substrate principle that preserves purity and enables the Schmidt bound underlying pageCurveFromUnitarity. Metric (inner-product) unitarity remains a stated future refinement; microscopic Hamiltonian derivation of the entropy readout is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.