operator_page_curve_one_statement
plain-language theorem explainer
Packages three facts into one citation target: a Schmidt-saturated operator Page process exists on the one-bit bulk/radiation types, the operator-derived Page-curve proposition holds, and a master-theorem PageCurveDerived witness is inhabited. Gravity-track authors cite it when they need the operator route rather than a supplied readout-equality field. The proof is a three-component term pairing the inhabitedness, proposition, and witness lemmas.
Claim. There exists a Schmidt-saturated operator Page process on bulk and radiation types $\mathrm{Fin}\,1$, the operator-derived Page-curve proposition holds (existence of such a process whose entropy readout has the Page-curve properties), and the master-theorem structure asserting a dynamical Page-curve derivation is inhabited.
background
Gravity Track 3.C upgrades the Page-curve story from a supplied readout field to an operator derivation. Earlier, PageCurveDynamical shipped the triangular Page curve as a Schmidt-capacity minimum and fed the master theorem via a witness that carried readout_eq_page_curve as an input field. This module instead defines the Schmidt capacity bound from the operator process, proves that saturation (entropy equals that bound) forces the Page-curve equality, and builds a witness that never names that field.
A Schmidt-saturated operator process extends an operator Page process by an entropy functional entropyFromState on the bulk-radiation ledger, with initial entropy zero and the saturation law: after $n$ unitary ticks the entropy equals the Schmidt capacity bound. The operator-derived proposition asserts existence of such a process on $(\mathrm{Fin},1,\mathrm{Fin},1)$. The master-theorem structure PageCurveDerived is the Track 3.C hypothesis interface whose holds field records that a dynamical Page-curve derivation has been established as a Lean theorem rather than a placeholder.
proof idea
Term-mode triple pairing. The first conjunct is discharged by schmidtSaturatedProcess_inhabited, which exhibits the canonical Schmidt-saturated process on $(\mathrm{Fin},1,\mathrm{Fin},1)$. The second is operatorDerivedPageCurveProp_holds, which packages that same canonical process into the existential proposition. The third wraps operatorPageCurveDerivedWitness in a Nonempty constructor; that witness sets page_curve_derived to the conjunction of the recognition-tick capacity-transfer law and the operator-derived proposition, with both halves already proved. No further rewriting or case analysis.
why it matters
This is the one-line citation surface for the operator-derived Page-curve track. Downstream load-bearing gravity theorems can point here instead of depending on any structure field literally named readout_eq_page_curve. The module doc states the design goal explicitly: the master-theorem witness from this module supersedes the field-based witness.
In the broader Recognition Science gravity program this closes the structural half of Track 3.C (Page curve as derived entropy of a unitary bulk-radiation process under Schmidt saturation). The Page-time $M^3$ scaling is already closed elsewhere; the remaining open work flagged on PageCurveDerived is the full dynamical entropy evolution (replica-wormhole / quantum-extremal-surface comparison). This declaration does not finish that physics, but it removes the scaffolding dependency on a supplied equality field and records that the operator route is inhabited end-to-end.
No downstream users are wired yet (used_by is empty), so the immediate role is archival packaging for the master theorem and future gravity-track imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.