schmidtSaturated_entropy_eq_pageCurve
plain-language theorem explainer
Radiation entropy at tick n of a Schmidt-saturated operator Page process equals the ledger-tick Page curve (min of bulk and radiation capacities). Gravity and holography workers cite it as the derived readout: entropy is read from the evolved state, not supplied by a free field. The proof is a one-line application of the process saturation hypothesis.
Claim. Let $P$ be a Schmidt-saturated operator Page process on finite bulk and radiation types, with black-hole entropy scale $S_{BH}$ and total tick count $N$. For every tick $n\le N$, the entropy functional applied to the bulk-radiation ledger after $n$ unitary ticks equals the ledger-tick Page curve $\min(\text{bulk capacity},\text{radiation capacity})$ at $(S_{BH},N,n)$.
background
Module Gravity Track 3.C derives Page radiation entropy from an operator process rather than from a supplied readout field. PageCurveDynamical already defines the triangular Page curve as a Schmidt-capacity minimum and iterates reversible Page ticks on a bulk-radiation ledger.
pageCurveFromLedgerTicks S_BH N n is the smaller of remaining-bulk capacity and emitted-radiation capacity at tick $n$. stateAfterOperatorTicks U n Ψ iterates the unitary tick map $U$ from an initial ledger $Ψ$.
A SchmidtSaturatedOperatorProcess extends an operator Page process by an entropy functional entropyFromState on ledgers, with zero entropy on the initial state, and a saturation axiom: after $n$ ticks the entropy equals the Schmidt capacity bound of the underlying process. Saturation is the only load-bearing hypothesis that forces the readout.
proof idea
One-line term proof. Apply the structure field saturates of $P$ at the given tick $n$ under the hypothesis $n\le N$. By definition of Schmidt saturation, entropy of the evolved ledger equals the Schmidt capacity bound, which is the ledger-tick Page curve, so the claimed equality is immediate.
why it matters
This is the derived readout theorem of Track 3.C: no readout_eq_page_curve field is required. Downstream, schmidtSaturated_entropy_zero rewrites at $n=0$ to get initial entropy zero; schmidtSaturated_entropy_full rewrites at full evaporation to recover return to zero; schmidtSaturated_entropy_peak rewrites at the half-evaporation Page fraction to obtain the peak $S_{BH}/2$.
Together these close the operator-derived witness path that supersedes the field-based master-theorem witness from PageCurveDynamical. In the Recognition gravity track this keeps the Page curve as a structural consequence of Schmidt saturation under unitary ledger ticks, not an independent postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.