PageCurveOperatorProcessCert
plain-language theorem explainer
Bundles the operator-level Page-process interface: nonempty bulk⊗radiation carrier, reversible ℂ-linear tick, entropy readout tied to the ledger Page curve, tick-by-tick state evolution, and radiation entropy zero at both ends of evaporation. Gravity Track 3.C cites it when closing the dynamical Page-curve story. It is a structure of obligations, not a proved identity.
Claim. A certificate asserting: (i) the bulk$\otimes$radiation Hilbert carrier on one-dimensional factors is inhabited; (ii) a reversible $\mathbb{C}$-linear Page tick (with linear inverse) exists on that carrier; (iii) an entropy readout exists whose radiation entropy at each tick equals the ledger-tick Page curve; (iv) every operator Page process evolves by applying its unitary tick once per step; (v) radiation entropy is $0$ at tick $0$ and at the final evaporation tick.
background
Module Gravity.PageCurveDynamical (Track 3.C) replaces the Session-101 kinematic triangular ansatz with a derived Page curve. Evaporation fraction $t\in[0,1]$ shrinks bulk capacity as $S_{BH}(1-t)$ and grows radiation capacity as $S_{BH},t$. Unitary evolution from a pure joint state plus Schmidt balance forces radiation entropy to equal $\min$ of those capacities, which is the triangle peaking at $t=1/2$.
The bulk-radiation carrier is the tensor product of bulk and Hawking-radiation ledgers. A Page tick is algebraic unitarity: a $\mathbb{C}$-linear map with a linear inverse satisfying both inverse laws (metric inner-product preservation is deferred). An operator Page process packages $S_{BH}\ge 0$, a positive tick budget, that unitary tick, and an initial joint state. The entropy readout extends the process by a function of tick index forced equal to the ledger-tick Page curve.
This certificate freezes those interface pieces at the minimal finite types $\mathrm{Fin},1$, plus the dynamical and boundary laws the readout must obey.
proof idea
No proof body: this is a structure definition. Each field is an interface obligation. Existence fields are Nonempty wrappers on the carrier, the reversible tick, and the entropy readout. The evolution field requires that the process state at step $n+1$ is the unitary tick applied to the state at $n$. The two readout fields require radiation entropy zero at the initial tick and at totalTicks. Downstream, a single noncomputable witness fills every field from prior inhabited lemmas and the structural readout proposition.
why it matters
Closes the operator-facing half of Track 3.C: the Page curve is no longer a hand-drawn piecewise linear function, but the entropy readout of a unitary bulk-radiation process. Downstream, pageCurveOperatorProcessCert supplies an explicit witness and pageCurveOperatorProcessCert_inhabited records that the certificate type is nonempty; the module's one-statement operator interface rests on that inhabitation.
In the RS gravity stack this sits above the structural ledger capacities and below any future metric refinement of the tick (inner-product preservation). It does not invoke the forcing chain T0–T8 or the RCL directly; its role is black-hole information bookkeeping under unitary eight-tick-compatible discrete time. The remaining open surface is deriving the entropy readout from a concrete microscopic Hamiltonian rather than equating it by interface to the ledger Page curve.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.