pageCurveOperatorEntropyCert
plain-language theorem explainer
Certificate that packages the operator-derived Page-curve master witness: a Schmidt-saturated operator process exists, the derived Page-curve proposition holds, and the master hypothesis routes through that derivation rather than a supplied readout field. Gravity-track consumers cite it to discharge the Page-curve master hypothesis without field-based readout equality. The body is a four-field structure instance wiring inhabitedness, the derived-prop theorem, the master witness, and a trivial True.
Claim. There is a certificate asserting: (i) a Schmidt-saturated operator process on unit finite types is inhabited; (ii) the operator-derived Page-curve proposition holds; (iii) a master-theorem Page-curve-derived witness is available whose derived clause is the conjunction of the recognition-tick capacity-transfer law and that operator-derived proposition; (iv) the witness does not rely on a supplied readout-equality field.
background
Gravity Track 3.C upgrades the Page curve from a supplied readout field to an operator-derived statement. The sibling module PageCurveDynamical already ships the triangular Page curve as a Schmidt-capacity minimum and a master-theorem witness that still carries readout_eq_page_curve as an input field. This module closes that gap.
Schmidt capacity is the min-bound on bipartite entanglement entropy for an operator process; saturation means entropy equals that capacity bound at every fraction. A Schmidt-saturated operator process is one for which that equality holds identically, so the entropy trajectory is forced to the triangular Page curve (zero at empty and full cut, peak at half).
The certificate structure records four obligations: inhabitedness of such a saturated process on Fin 1 × Fin 1, the operator-derived Page-curve proposition, a PageCurveDerived master witness whose payload is the conjunction of the recognition-tick capacity-transfer law with that proposition, and an explicit True flag that the witness does not use the old readout field.
proof idea
Pure structure construction. The four fields are filled by existing results: inhabitedness by schmidtSaturatedProcess_inhabited (which wraps the canonical saturated process), the derived proposition by operatorDerivedPageCurveProp_holds (again via the canonical process), the master witness by operatorPageCurveDerivedWitness (conjunction of recognition-tick transfer and the operator-derived prop, both already proved), and the no-readout-field flag by trivial. No new algebra is performed.
why it matters
This is the load-bearing certificate of Track 3.C. Downstream, pageCurveOperatorEntropyCert_inhabited simply packages it as Nonempty, feeding the one-statement operator-derived Page-curve claim: the saturated process exists, the derived readout has all Page-curve properties, and no theorem depends on a field literally named readout_eq_page_curve.
In the broader Recognition gravity stack this closes the structural gap between dynamical Schmidt capacity and the master-theorem interface. The Page curve itself is not re-derived here; what changes is the provenance of the equality, from an assumed readout field to a saturation theorem on the operator process. That provenance matters for any later claim that the Page curve is forced rather than fitted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.