pageCurveOperatorProcessCert_inhabited
plain-language theorem explainer
The operator-level Page process certificate is inhabited: there is a concrete bulk-radiation carrier, a reversible complex-linear Page tick, iterated states evolving by that tick, and an entropy readout linking the operator process to the ledger-tick Page curve. Gravity and black-hole information workers cite it as the existence witness for the dynamical interface. The proof is a one-line term that supplies the prebuilt certificate instance.
Claim. There exists a certificate for the operator-level Page process interface: a nonempty bulk-radiation ledger carrier on unit finite types, a nonempty reversible $\mathbb{C}$-linear Page tick unitary on that carrier, a nonempty operator entropy readout connecting the process to the ledger-tick Page curve, and the evolution law that every operator Page process advances by applying its unitary tick at each successive natural-number step.
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 bulk$\otimes$radiation state plus Schmidt balance forces radiation entropy to equal $\min$ of the two capacities, which is the triangular Page curve peaking at $t=1/2$.
The certificate packages four interface pieces: a bulk-radiation ledger carrier, a unitary Page tick (reversible $\mathbb{C}$-linear operator), an entropy readout from operator process to ledger-tick curve, and the discrete evolution law that the state at tick $n+1$ is the tick applied to the state at $n$. Upstream constants fix the RS time quantum $\tau_0=1$ tick; foundation entropy is total defect, zero at the minimum-entropy initial state. The structural sibling module only gave a kinematic ansatz; this track supplies the dynamical recipe.
proof idea
One-line term proof. The goal is Nonempty of the certificate structure; the proof is the anonymous constructor applied to the already-defined witness pageCurveOperatorProcessCert, which fills the four fields (carrier, unitary tick, entropy readout, and the tick-evolution identity). No tactics, no further lemmas in the body.
why it matters
Closes the existence side of the operator-level Page process interface in Track 3.C: bulk-radiation carrier explicit, Page tick reversible and linear, iterated states evolve by that tick, and an entropy readout ties the operator process to the ledger-tick Page curve. That is the dynamical upgrade over Session 101's hand-drawn triangular ansatz. Downstream uses are not yet wired (used_by empty). The module doc and the one-statement comment are explicit that this is not master-clause readiness: deriving the readout from a specific microscopic Hamiltonian or recognition update remains open. Framework landmarks in view are unitary evolution preserving purity (hence Schmidt balance) and the eight-tick octave as the fundamental evolution period; the certificate itself stays at the process-interface layer rather than forcing T5-T8 constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.