operatorDerivedPageCurveProp_holds
plain-language theorem explainer
The operator-derived Page-curve proposition holds: a Schmidt-saturated operator process exists from which the triangular Page curve is recovered as process entropy, without a supplied readout field. Gravity and holography workers citing the RS operator route to the Page curve use this existence fact. The proof is a one-line term exhibiting the canonical single-tick saturated process and discharging the residual goal by triviality.
Claim. The operator-derived Page-curve proposition is true: there exists a Schmidt-saturated operator process on the bipartite cut $\mathrm{Fin}\,1\otimes\mathrm{Fin}\,1$ with unit black-hole entropy budget and a single recognition tick, from which the Page-curve entropy law is recovered by saturation (entropy equals the Schmidt capacity bound).
background
Gravity Track 3.C upgrades the Page-curve story from a supplied readout field to an operator derivation. The dynamical module already packages the triangular Page curve as a Schmidt-capacity minimum $\min(\mathrm{bulkCap},\mathrm{radCap})$ and offers a master-theorem witness that still carries readout_eq_page_curve as an input field. This module removes that load-bearing field.
A Schmidt-saturated operator process is an operator process whose von Neumann (or RS) entropy equals the Schmidt capacity bound at every tick. Saturation is proved to force the Page-curve equalities (start at zero, return to zero, peak at the Page fraction). The canonical process used here lives on $\mathrm{Fin},1\otimes\mathrm{Fin},1$ with $S_{\mathrm{BH}}=1$ and totalTicks $=1$: the identity tick leaves the state fixed, so entropy is identically zero and the capacity bound is zero on both ticks, making saturation a two-point case split.
The fundamental RS time quantum is one tick ($\tau_0=1$). The operator-derived proposition is the existence claim that such a saturated process inhabits the type, so the derived readout path is non-vacuous.
proof idea
Term-mode pair constructor, not a tactic script. The first component is the canonical Schmidt-saturated operator process (the inhabited witness on $\mathrm{Fin},1\otimes\mathrm{Fin},1$ with unit budget and one tick). The second component is trivial, which closes the residual propositional obligation packaged inside the operator-derived proposition (the saturation and Page-curve identities are already proved inside that structure's fields). No further lemmas are invoked at the call site.
why it matters
This is the existence hinge that lets the module supersede the field-based Page-curve witness. Downstream, the operator Page-curve derived witness stores the conjunction of the recognition-tick capacity transfer law with this proposition, and routes the master-theorem PageCurveDerived record through that conjunction rather than through a supplied readout-equality field. The one-statement theorem packages inhabitedness of the saturated process, this proposition, and nonemptiness of the master witness as a single claim. The module certificate records the same triple and asserts that the witness does not use the readout field.
In the broader RS gravity track this closes the structural gap between dynamical Page entropy and operator entropy: the triangular curve is no longer an axiom of the readout, but a consequence of Schmidt saturation of an explicit process. It does not itself invoke the forcing chain (T5–T8) or the RCL; it sits downstream as a gravity-side structural theorem (0 sorry, 0 RS-internal axiom).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.