pageCurveOperatorProcessCert
plain-language theorem explainer
Explicit witness that the operator-level Page process certificate is inhabited on the minimal bulk–radiation carrier (one-dimensional factors). Gravity and information theorists citing the one-statement operator Page interface use this packing. The body fills each certificate field from preexisting nonempty instances and tick/readout lemmas.
Claim. There is an explicit operator-level Page process certificate on bulk and radiation factors of type $\mathrm{Fin}\,1$: the bulk–radiation ledger is nonempty, a unitary Page tick exists, an entropy readout exists, the process state at tick $n+1$ equals the unitary tick applied to the state at $n$, radiation entropy at tick $0$ is $0$, and radiation entropy at the final tick is $0$.
background
Module Gravity Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation fraction $t\in[0,1]$ transfers entropy from bulk to radiation; bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ and radiation capacity rises as $S_{\mathrm{BH}}t$. Purity of the joint state plus Schmidt balance force radiation entropy to equal $\min$ of those capacities, which is the Page triangle.
The certificate structure packages the operator interface: a nonempty bulk–radiation ledger, a nonempty unitary tick, a nonempty entropy readout, and three process laws (tick evolution; readout zero at start and full evaporation). Upstream, pageTickUnitary_inhabited supplies the identity tick; operator_level_page_process_structural_prop_holds supplies the canonical readout; stateAtTick_succ, radiationEntropyAtTick_zero, and radiationEntropyAtTick_full discharge the three laws.
proof idea
Field-by-field construction of the certificate record, not a deep argument. Bulk–radiation carrier is the trivial nonempty witness on $\mathrm{Fin},1\times\mathrm{Fin},1$. Unitary tick is pageTickUnitary_inhabited (identity tick). Entropy readout is the theorem that the operator-level structural property holds (canonical readout at dimension 1). The three process fields are direct applications of stateAtTick_succ, radiationEntropyAtTick_zero, and radiationEntropyAtTick_full as function values.
why it matters
Closes the operator-level Page process interface as a single packed witness. Downstream, pageCurveOperatorProcessCert_inhabited is the one-line Nonempty theorem that cites this def; its doc frames the bulk–radiation carrier, reversible $\mathbb{C}$-linear tick, and entropy readout as the operator interface one-statement. In the module arc this sits above the kinematic Session-101 ansatz: the triangular curve is already derived from unitarity and Schmidt balance, and this certificate records that the dynamical operator process exists on the minimal carrier. It does not itself re-prove the min-capacity shape; it certifies the process layer that those capacity lemmas feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.