schmidtSaturatedProcess_inhabited
plain-language theorem explainer
The type of Schmidt-saturated operator Page processes on a one-by-one bulk/radiation ledger is inhabited. Anyone citing the operator-derived Page-curve one-statement or the Gravity Track 3.C certificate needs this existence witness. The proof is a one-line term that packages the canonical single-tick process.
Claim. There exists a Schmidt-saturated operator Page process on bulk and radiation types $\mathrm{Fin}\,1$ and $\mathrm{Fin}\,1$: an operator process equipped with a state-derived entropy functional that vanishes on the initial ledger and, at every tick up to the budget, equals the Schmidt capacity bound $\min(n\cdot S_{\mathrm{BH}}/N,\,S_{\mathrm{BH}}-n\cdot S_{\mathrm{BH}}/N)$.
background
Gravity Track 3.C replaces a field-supplied Page readout with an operator-derived one. Earlier, PageCurveDynamical gave the triangular Page curve as a Schmidt-capacity minimum and a master-theorem witness that still carried readout_eq_page_curve as an input field. This module defines the capacity bound from the process, proves that saturation forces the Page equality, and builds a witness that never loads that field.
A Schmidt-saturated operator process extends an operator Page process by a functional entropyFromState on the bulk/radiation ledger. It must vanish on the initial state, and at every tick $n\le N$ the entropy of the evolved state must equal the Schmidt capacity bound of the underlying process. The entropy is therefore derived from the state, not an independent curve.
The canonical witness is the single-tick process on $\mathrm{Fin},1\otimes\mathrm{Fin},1$ with $S_{\mathrm{BH}}=1$ and identity tick: every state maps to entropy $0$, and the Page curve is identically $0$ on ${0,1}$, so saturation is immediate by case split.
proof idea
One-line term proof. The goal is Nonempty (SchmidtSaturatedOperatorProcess (Fin 1) (Fin 1)). Supply the already-constructed canonicalSchmidtSaturatedProcess as the witness via the anonymous constructor ⟨...⟩. No further tactics or lemmas are needed at this site; all saturation and zero-entropy obligations were discharged inside that definition.
why it matters
Existence of a saturated process is the first conjunct of the operator-derived Page-curve one-statement: the process exists, the derived readout has the Page properties (zero, return-to-zero, peak at Page fraction), and the master-theorem witness routes through the operator derivation without a supplied readout_eq_page_curve field. The certificate pageCurveOperatorEntropyCert records the same inhabitation fact as its first field.
In the module's own terms, this closes the structural gap between "Page curve as a named field" and "Page curve forced by Schmidt saturation of a state-derived entropy." It is a minimal but load-bearing existence step in Gravity Track 3.C (structural theorem, zero sorry). It does not itself touch the T0–T8 forcing chain or the RCL; it sits in the gravity/Page-curve layer that consumes those foundations upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.