operatorPageCurveDerivedWitness
plain-language theorem explainer
Packages the operator-route Page-curve derivation as a master-theorem witness: recognition-tick capacity transfer together with existence of a Schmidt-saturated operator process whose entropy readout follows the Page curve. Gravity auditors cite it for a PageCurveDerived instance that does not rest on a supplied readout-equality field. The body is a pair of already-proved propositions.
Claim. A master-theorem witness asserting that (i) bulk and radiation capacities transfer by $S_{\mathrm{BH}}/N$ per recognition tick, with conserved total capacity and continuous Page curve at the tick-induced evaporation fraction, and (ii) there exists a Schmidt-saturated operator process whose derived entropy readout has the Page-curve properties. Both conjuncts hold.
background
Track 3.C of the gravity stack treats the Page curve as a structural theorem with no sorry and no RS-internal axiom. The dynamical module already ships the triangular Page curve as a Schmidt-capacity minimum and a master-theorem witness that still carries readout equality as a supplied field of an operator-page-entropy readout structure.
This module replaces that field dependence. It defines a Schmidt capacity bound from the operator process, proves that Schmidt saturation (entropy equals the capacity bound) implies Page-curve equality, and builds a witness that routes only through the derived theorem. The recognition-tick capacity transfer package states that bulk capacity drops by $S_{\mathrm{BH}}/N$ per emitted tick, radiation capacity rises by the same amount, total capacity is conserved, and the ledger-tick curve matches the continuous Page curve at the tick-induced evaporation fraction.
The master structure PageCurveDerived is the Track 3.C hypothesis interface: a proposition page_curve_derived together with a proof that it holds. The operator-derived proposition asserts existence of a Schmidt-saturated operator process (here on degenerate Fin 1 factors) with no readout-equality field in the chain.
proof idea
Definitional packaging, not a tactic proof. The page_curve_derived field is the conjunction of the recognition-tick capacity transfer proposition and the operator-derived Page-curve proposition. The holds field is the pair of the two existing theorems: the transfer package (radiation step, bulk step, conservation, curve identity) and the operator existence theorem, which inhabits the saturated process by the canonical Schmidt-saturated process and closes the existential with trivial.
why it matters
This is the operator-route master-theorem witness that supersedes the field-based dynamical witness: no load-bearing theorem needs a field literally named readout-equality. Downstream, the unconditional master theorem re-exports it as the canonical operator-route witness (retained for provenance on the degenerate Fin 1 route). The one-statement theorem packages inhabited saturated process, the operator-derived proposition, and nonempty master witness. The module certificate records inhabited saturation, the operator proposition, this witness, and the audit fact that the witness does not use the readout field.
In the broader RS gravity track this closes the structural side of Page-curve derivation while the full dynamical entropy evolution (unitary joint matter-radiation system, replica-wormhole / quantum-extremal-surface comparison) remains the open multi-session part of Track 3.C. The $M^3$ Page-time scaling is already closed; this witness keeps the operator path available without reopening the supplied-field route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.