canonicalSchmidtSaturatedProcess
plain-language theorem explainer
A minimal inhabited instance of a Schmidt-saturated operator Page process on one-dimensional bulk and radiation spaces with a single-tick budget. Entropy is constantly zero and the identity tick leaves the ledger fixed, so the Page curve collapses to zero at both ticks. Gravity-track proofs cite it to show the saturated-process type is nonempty and to feed the operator-derived Page-curve master witness. The construction is by direct field assignment plus a two-case saturation check.
Claim. There is a Schmidt-saturated operator Page process on $\mathrm{Fin}\,1 \otimes \mathrm{Fin}\,1$ with black-hole entropy $S_{\mathrm{BH}}=1$, total tick budget $N=1$, identity tick unitary, initial ledger state $0$, and state-derived entropy functional constantly $0$. For every tick $n\le 1$, that entropy equals the Schmidt capacity bound $\min(\mathrm{bulkCap},\mathrm{radCap})$ at the tick-induced evaporation fraction (which is identically $0$).
background
Gravity Track 3.C upgrades the dynamical Page curve from a supplied readout field to an operator-derived equality. An operator Page process carries black-hole entropy $S_{\mathrm{BH}}$, a total recognition-tick budget $N$, a reversible tick unitary on the bulk-radiation ledger, and an initial state. The ledger-tick Page curve is $\min$ of remaining bulk capacity $S_{\mathrm{BH}}(N-n)/N$ and emitted radiation capacity $S_{\mathrm{BH}} n/N$.
The Schmidt capacity bound is that same $\min$ evaluated on the process parameters: the maximum radiation entropy consistent with Schmidt purification of a pure joint state. A Schmidt-saturated operator process extends the bare process by a state-derived entropy functional that vanishes on the initial state and, at every tick $n\le N$, equals the Schmidt capacity bound after $n$ applications of the tick unitary.
The identity tick unitary is the minimal non-vacuous reversible operator (tick and untick both $\mathrm{id}$). It is not evaporation dynamics; it only witnesses that the operator interface is inhabited.
proof idea
Direct structure inhabitant. Set $S_{\mathrm{BH}}=1$, $N=1$, the identity tick on $\mathrm{Fin},1\otimes\mathrm{Fin},1$, initial state $0$, and constant-zero entropy-from-state. Nonnegativity and positivity of the tick budget are norm_num. Initial entropy zero is rfl.
Saturation: for $n\le 1$, unfold the Schmidt capacity bound to the ledger-tick Page curve and case-split on $n\in{0,1}$. Both bulk and radiation capacities evaluate to $0$ under $S_{\mathrm{BH}}=1$, $N=1$, so the $\min$ is $0$, matching the constant entropy functional.
why it matters
This is the concrete witness that Schmidt-saturated operator processes exist. Downstream, schmidtSaturatedProcess_inhabited packages it as Nonempty, and operatorDerivedPageCurveProp_holds feeds it into the operator-derived Page-curve master proposition: the master witness routes through saturation of a state-derived entropy functional rather than a supplied readout_eq_page_curve field.
Per the module status, Track 3.C is a structural theorem (zero sorry, zero RS-internal axiom). The canonical process closes the inhabitance gap so no load-bearing theorem depends on a hand-supplied readout equality. It is deliberately the trivial single-tick, identity-dynamics corner case: enough to discharge structural obligations, not a model of realistic evaporation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.