PageCurveOperatorEntropyCert
plain-language theorem explainer
Certificate packaging the operator-derived Page-curve track: a nonempty Schmidt-saturated operator process on unit bulk/radiation types, the operator-derived Page proposition, and a master-theorem witness that does not rely on a supplied readout-equality field. Gravity auditors cite it as the structural bundle for Track 3.C. It is a pure structure definition; inhabitation is discharged downstream by concrete witnesses.
Claim. A certificate is a record of four data: (i) the type of Schmidt-saturated operator Page processes on bulk and radiation labels $\mathrm{Fin}\,1$ is nonempty; (ii) the operator-derived Page-curve proposition holds (existence of such a saturated process); (iii) a master-theorem $PageCurveDerived$ witness is supplied; (iv) a trivial flag recording that the witness does not use a supplied readout-equality field.
background
Module Gravity Track 3.C upgrades the dynamical Page curve from a field-supplied readout to an operator-derived equality. Earlier, PageCurveDynamical gave the triangular Page curve as a Schmidt-capacity minimum and witnessed the master theorem via an OperatorPageEntropyReadout structure whose readout_eq_page_curve field was an input. This module instead defines a Schmidt capacity bound from the operator process, proves that saturation (entropy equals that bound) forces the Page-curve readout, and packages a witness that never names the old field.
A Schmidt-saturated operator process extends an operator Page process by an entropy functional entropyFromState on the bulk-radiation ledger, with zero initial entropy and the saturation law: after $n$ unitary ticks the entropy equals the Schmidt capacity bound. The operator-derived proposition is simply existence of such a process on $(\mathrm{Fin},1,\mathrm{Fin},1)$. Upstream, PageCurveDerived is the Track 3.C master hypothesis: a proposition plus a proof that it holds; the dynamical entropy evolution side remains multi-session work, while Page-time $M^3$ scaling is already closed.
proof idea
No proof body: the declaration is a structure (four fields). Inhabitation is not claimed here. Downstream, pageCurveOperatorEntropyCert fills the fields by schmidtSaturatedProcess_inhabited, operatorDerivedPageCurveProp_holds, the concrete operatorPageCurveDerivedWitness (conjunction of recognition-tick capacity transfer and the operator-derived prop), and trivial for the readout-field flag. The companion theorem then wraps that value as Nonempty.
why it matters
This is the master-cert interface for operator-derived Page entropy. It lets the framework supersede any load-bearing dependence on a field literally named readout_eq_page_curve: the witness routes through Schmidt saturation and the derived equality instead. Downstream, pageCurveOperatorEntropyCert and pageCurveOperatorEntropyCert_inhabited produce a concrete inhabited certificate and the one-statement operator-derived Page-curve claim. In the broader RS gravity track it closes the structural half of Track 3.C (0 sorry, 0 RS-internal axiom in this module) while leaving the heavy dynamical entropy evolution inside PageCurveDerived as the remaining open multi-session obligation. No direct T0–T8 forcing step is claimed; the link is the recognition-tick capacity transfer bundled into the master witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.