S_rad_nonneg
plain-language theorem explainer
Radiation entropy stays non-negative on the full evaporation interval: for every real t with 0 ≤ t ≤ 1, S_rad(t) ≥ 0. Anyone checking the dynamical Page-curve package against the structural axioms cites this bound. The proof rewrites S_rad via Schmidt purification and hands the claim to the already-proved non-negativity of the unitarity Page curve.
Claim. Let $P$ be a dynamical Page-curve process. For every real $t$ with $0 \le t \le 1$, the radiation entropy satisfies $0 \le S_{\mathrm{rad}}(t)$.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterised by $t \in [0,1]$: the fraction of total entropy transferred from bulk to radiation. Bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ and radiation capacity rises as $S_{\mathrm{BH}},t$.
Unitarity keeps the joint bulk⊗radiation state pure, so Schmidt's theorem forces $S(\rho_{\mathrm{bulk}})=S(\rho_{\mathrm{rad}})$ and both are bounded by $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$. Under maximal Schmidt balance the radiation entropy saturates that min, which is exactly the triangular Page curve.
Upstream, pageCurveFromUnitarity_nonneg already records non-negativity of that min expression whenever $S_{\mathrm{BH}}\ge 0$ and $t\in[0,1]$. The process field $S_{\mathrm{rad}}$ is identified with the unitarity curve by the Schmidt-purification equation.
proof idea
Term-mode, two steps. First rewrite $P.S_{\mathrm{rad}},t$ by the process equation schmidt_purification, which equates radiation entropy to the unitarity Page-curve expression. Then apply pageCurveFromUnitarity_nonneg to that expression, feeding $P.S_{\mathrm{BH_nonneg}}$ together with the interval hypotheses $0\le t\le 1$. No further arithmetic is needed.
why it matters
Non-negativity is one of the elementary sanity checks that the derived dynamical Page curve must pass before it can stand in for the structural ansatz of Session 101. Downstream, page_curve_derived_dynamical_prop_holds packages the canonical process and its boundary/peak values; the same non-negativity obligation sits inside that property bundle.
In the broader Recognition gravity track this closes a fragment of Track 3.C: the triangular shape (ascent, peak at half-evaporation, return to zero) is forced by unitarity plus Schmidt balance, not drawn by hand. The result is fully proved (zero sorry) and does not touch the forcing chain T0–T8 or the RCL directly; it is a gravity-side consequence of the ledger/unitarity substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.