S_rad_at_one
plain-language theorem explainer
At full evaporation (parameter t = 1), the radiation von Neumann entropy of a Schmidt-balanced Page process is exactly zero. Anyone citing unitary information return or the late-time leg of the dynamical Page curve needs this endpoint. The proof is a two-step rewrite: Schmidt purification reduces S_rad to the unitarity Page function, which vanishes at t = 1 once black-hole entropy is nonnegative.
Claim. For a Schmidt-balanced dynamical Page process $P$ with nonnegative black-hole entropy, the radiation entropy satisfies $S_{\mathrm{rad}}(1) = 0$.
background
Track 3.C derives the triangular Page curve from ledger dynamics rather than postulating it. Evaporation is parameterized by $t \in [0,1]$: the fraction of total entropy transferred from bulk to radiation. Bulk capacity falls as $S_{\mathrm{BH}}(1-t)$; radiation capacity grows as $S_{\mathrm{BH}}, t$.
The joint bulk$\otimes$radiation state stays pure under unitary evolution from a pure initial bulk. Schmidt's theorem then forces $S(\rho_{\mathrm{bulk}}) = S(\rho_{\mathrm{rad}})$, each bounded by $\min(\log d_{\mathrm{bulk}}, \log d_{\mathrm{rad}})$. Under maximal Schmidt balance the radiation entropy saturates that bound, so $S_{\mathrm{rad}}(t) = \min(\mathrm{bulkCapacity}, \mathrm{radiationCapacity})$.
At $t = 1$ the bulk Hilbert space has collapsed (capacity zero) while the radiation space holds the full ledger. Purity plus the capacity bound force the reduced radiation state to be pure, hence zero entropy: information has returned.
proof idea
Term-mode, two rewrites. First apply the process's Schmidt-purification identity, which identifies $P.S_{\mathrm{rad}}$ with the unitarity Page curve built from the two linear capacities. Then invoke the endpoint lemma pageCurveFromUnitarity_at_one, using nonnegativity of $P.S_{\mathrm{BH}}$: at $t = 1$ one has $\min(S_{\mathrm{BH}}(1-1), S_{\mathrm{BH}}\cdot 1) = \min(0, S_{\mathrm{BH}}) = 0$.
why it matters
This is the late-time anchor of the dynamical Page curve. Downstream, S_rad_information_returned is the named citation form of the same fact, and page_curve_derived_dynamical_prop_holds packages the three checkpoints (ascent start, Page peak, full return) into the structural proposition that the triangular curve is derived, not assumed.
Together with the $t = 0$ vanishing and the $t = 1/2$ peak at $S_{\mathrm{BH}}/2$, it closes the kinematic gap left by Session 101's hand-drawn ansatz: the return of radiation entropy to zero is forced by Schmidt purity plus linear capacity transfer. In the broader Recognition gravity track this is the information-return leg of unitary black-hole evaporation on the ledger, with no extra RS axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.