schmidtSaturated_entropy_full
plain-language theorem explainer
At full evaporation of a Schmidt-saturated operator Page process, the radiation entropy derived from the bulk-radiation state is exactly zero. Anyone citing the operator-derived Page curve (Track 3.C) uses this endpoint identity. The proof rewrites via the saturation-to-Page equality and applies the ledger Page-curve vanishing at full tick count.
Claim. Let $P$ be a Schmidt-saturated operator Page process on finite bulk and radiation types. After $P$ has run for its full tick count from the initial bulk-radiation ledger, the entropy functional of $P$ evaluated on that final state equals $0$.
background
Gravity Track 3.C replaces a supplied Page-curve readout field by a derived equality. An operator Page process evolves a bulk-radiation ledger by iterating a reversible unitary tick. The triangular Page curve is the Schmidt-capacity minimum over emitted-tick fraction; at full evaporation that capacity vanishes, so the ledger Page curve is zero (pageCurveFromLedgerTicks_at_full).
A Schmidt-saturated operator process extends the operator process by an entropy functional of the state, forced to equal the Schmidt capacity bound at every tick up to the total count. The sibling theorem schmidtSaturated_entropy_eq_pageCurve then identifies that state entropy with the ledger Page curve, without any independent readout_eq_page_curve field.
proof idea
Two-step rewrite. First apply the derived readout theorem: at $n = $ total ticks (hypothesis le_rfl), state entropy equals pageCurveFromLedgerTicks of $(S_{BH}, N, N)$. Then invoke pageCurveFromLedgerTicks_at_full with nonnegativity of $S_{BH}$ and positivity of the total tick count from the process structure, which returns $0$.
why it matters
Closes the late-time endpoint of the operator-derived Page curve: after complete evaporation the radiation entropy readout is zero, matching unitarity and the triangular Page shape. Together with the zero-tick and Page-fraction siblings it pins the three canonical points of the curve from Schmidt saturation alone.
The module status is structural (0 sorry, 0 RS-internal axiom). Downstream, this supports the master-theorem witness that supersedes field-based readout_eq_page_curve witnesses from PageCurveDynamical. No further used-by edges are recorded yet; the result is an endpoint lemma for the saturation package rather than a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.