SchmidtSaturatedOperatorProcess
plain-language theorem explainer
A Schmidt-saturated operator Page process is an operator-level bulk-radiation evolution equipped with a state-derived entropy map that equals the Schmidt capacity bound at every tick up to the evaporation budget. Anyone proving an operator-derived Page curve (without a supplied readout-equality field) cites this interface. It extends the plain operator Page process by three fields: the entropy functional, initial zero entropy, and the saturation axiom. As a structure definition there is no proof body.
Claim. A Schmidt-saturated operator Page process on finite bulk and radiation types $\beta,\rho$ is an operator Page process together with a map $S$ from the bulk-radiation ledger to $\mathbb{R}$ such that $S$ of the initial state is $0$, and for every $n\le N$ (the evaporation tick budget) the entropy of the state after $n$ unitary ticks equals the Schmidt capacity bound of the underlying process at tick $n$.
background
Track 3.C (this module) upgrades the dynamical Page setup so the entropy readout is derived from the operator process rather than asserted by a field. Upstream, an operator Page process packages a closed bulk-radiation ledger (bulk ledger tensor Hawking-radiation ledger over $\mathbb{C}$), a nonnegative black-hole entropy $S_{BH}$, a positive finite tick budget $N$, an initial state, and a reversible linear tick operator. The ledger is the Lean-facing carrier for bulk plus radiation requested by the track.
The Schmidt capacity bound is the triangular $\min$ built from that process; it is the shape that becomes the Page curve once entropy is forced to match it. In the broader foundation, configuration entropy is proportional to total defect (zero defect is minimum entropy). Here the entropy map is an abstract functional of the ledger state after unitary ticks, not that defect formula.
Saturation is the structural hinge: once entropy tracks capacity at every tick, Page-curve equality is a theorem about the process, not an independent readout hypothesis.
proof idea
Structure definition, not a proved theorem. It extends the operator Page process with three fields: (1) a real-valued entropy functional on bulk-radiation ledger states; (2) the requirement that this functional vanishes on the initial state; (3) the saturation axiom, that for every $n\le N$ the entropy after $n$ applications of the unitary tick equals the Schmidt capacity bound of the underlying process. Downstream equalities (entropy equals the Page curve; zero at start and full evaporation; peak at the Page fraction) are immediate rewrites or one-line applications of the saturation field together with properties of the capacity bound.
why it matters
This interface is what lets Track 3.C claim a derived Page readout with zero sorry and no RS-internal axiom. Downstream theorems apply saturation to obtain entropy equal to the Page curve, vanishing at $n=0$ and at full evaporation, and peaking at the Page fraction. The canonical single-tick process on $\mathrm{Fin},1\otimes\mathrm{Fin},1$ inhabits the structure; the operator-derived proposition is mere existence of such a process; the certificate and one-statement theorem package inhabitation, that proposition, and a master-theorem witness that routes through the operator derivation rather than a field named readout-equals-Page-curve.
In the Recognition gravity track this closes the structural gap between unitary ledger evolution and the triangular Page curve: the master witness supersedes the field-based witness from the dynamical module. No new continuum or Hamiltonian content is added; the gain is purely that load-bearing theorems no longer depend on a supplied readout equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.