operator_level_page_process_structural_prop_holds
plain-language theorem explainer
The operator-level Page-process structural property is inhabited: there exists a bulk-radiation entropy readout on the minimal one-slot carriers. Gravity and Page-curve workers cite it to discharge the Nonempty half of the operator interface. The proof is a one-line term that builds the canonical readout at unit black-hole entropy and a single tick.
Claim. There exists an operator Page-entropy readout on the one-dimensional bulk and radiation carriers $(\mathrm{Fin}\,1)\otimes(\mathrm{Fin}\,1)$: a structure carrying a nonnegative black-hole entropy $S_{\mathrm{BH}}$, a positive total tick count, and the interface that connects reversible tick evolution to the ledger Page curve.
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_{\mathrm{BH}}(1-t)$ and radiation capacity rises as $S_{\mathrm{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 triangle peaking at $t=1/2$.
The operator layer sits above that kinematic story. An operator Page-entropy readout packages $S_{\mathrm{BH}}\ge 0$, a positive tick budget, and the maps that read entropy off iterated states of a reversible $\mathbb{C}$-linear tick on an explicit bulk-radiation carrier. The structural proposition simply asserts that this readout type is nonempty on the minimal carriers $\mathrm{Fin},1$.
Upstream, the canonical readout witness is defined precisely to inhabit that interface using only the identity tick; it "does not claim physical evaporation dynamics." Finite-dimensional Stone/Hamiltonian emergence and self-reference scaffolding appear in the dependency cone but are not invoked in the body of this theorem.
proof idea
Term-mode existence proof. The goal is $\mathrm{Nonempty}(\mathrm{OperatorPageEntropyReadout},(\mathrm{Fin},1),(\mathrm{Fin},1))$. Supply the canonical readout at $S_{\mathrm{BH}}=1$ (nonnegativity by norm_num) and total ticks $N=1$ (positivity by norm_num). That single constructor application is the entire proof; no further lemmas are unfolded.
why it matters
Closes the entropy-readout conjunct of the operator-level Page process interface. Downstream, pageCurveOperatorProcessCert installs this theorem as its entropy_readout field, and operator_page_process_interface_one_statement conjoins it with inhabited bulk-radiation carrier, inhabited unitary tick, tick-evolution of states, and zero initial radiation entropy.
In the Recognition gravity track this is the structural bridge from the Session-101 kinematic triangle to an explicit operator process on a finite carrier. It does not yet derive the readout from a microscopic Hamiltonian or recognition update; that remains the open master-clause gap noted in the one-statement theorem. Framework landmarks touched only indirectly: unitary finite-dimensional evolution (eight-tick register spirit) and ledger capacity accounting that ultimately feeds mass/gravity phenomenology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.