operatorDerivedPageCurveProp
plain-language theorem explainer
The operator-derived Page-curve proposition is the bare existence claim that a Schmidt-saturated operator process lives on unit bulk and radiation types. Downstream master-theorem witnesses cite it to route Page-curve entropy through state-derived saturation rather than a supplied readout field. The definition is an existential over that structure with a trivial payload.
Claim. There exists a Schmidt-saturated operator Page process on bulk and radiation types of cardinality one (finite, decidable) such that entropy is read from the bulk-radiation ledger state, starts at zero, and saturates the Schmidt capacity bound at every tick; the proposition itself carries no further constraints beyond that existence.
background
Gravity Track 3.C replaces a field-supplied Page-curve readout with an operator derivation. Upstream, PageCurveDynamical already gives 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.
A Schmidt-saturated operator process extends an operator Page process by an entropy functional entropyFromState on the bulk-radiation ledger. Saturation means radiation entropy at each tick equals the Schmidt capacity bound built from the process; initial entropy is zero. The doc-comment stresses that entropy is derived from the state, not supplied independently, so saturation forces the readout onto the Page curve.
This proposition packages that existence claim for the unit types Fin 1, Fin 1, which is the canonical witness size used throughout the module.
proof idea
Not a proof: a propositional abbreviation. It is the existential ∃ _ : SchmidtSaturatedOperatorProcess (Fin 1) (Fin 1), True. Inhabitation is discharged later by canonicalSchmidtSaturatedProcess inside operatorDerivedPageCurveProp_holds; the True payload is filled by trivial.
why it matters
This is the hinge that lets the module supersede field-based Page-curve witnesses. operatorDerivedPageCurveProp_holds proves it; operatorPageCurveDerivedWitness conjoins it with the recognition-tick capacity transfer law to build a PageCurveDerived master-theorem record whose page_curve_derived field never mentions readout_eq_page_curve. The one-statement theorem and PageCurveOperatorEntropyCert both re-export the same existence claim.
In the broader RS gravity track this closes the structural gap between operator evolution and the triangular Page curve (entropy starts at zero, returns to zero, peaks at the Page fraction) without an external equality hypothesis. It is scaffolding-free (0 sorry) and feeds only certified master-theorem packaging, not a new physical constant or forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.