S_rad_at_zero
plain-language theorem explainer
Radiation entropy vanishes at the start of evaporation: when the transferred-entropy fraction is zero, S_rad equals zero. Anyone checking the dynamical Page-curve boundary conditions cites this. The proof is a two-step rewrite through Schmidt purification into the unitarity Page formula evaluated at t = 0.
Claim. For a Schmidt-purified bulk-radiation process $P$ with nonnegative black-hole entropy, the radiation entropy satisfies $S_{\mathrm{rad}}(0) = 0$.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterized by $t \in [0,1]$: the fraction of total entropy moved from bulk to radiation. At $t = 0$ the hole is intact; at $t = 1$ it has fully evaporated.
Bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ and radiation capacity grows as $S_{\mathrm{BH}}, t$. Unitarity keeps the joint bulk $\otimes$ radiation state pure, so Schmidt's theorem forces equal reduced entropies bounded by $\min$ of the two capacities. Under maximal Schmidt balance the radiation entropy saturates that bound, yielding the triangular curve.
Upstream, pageCurveFromUnitarity_at_zero already shows the abstract unitarity formula evaluates to zero at $t = 0$: after unfolding, bulk capacity is $S_{\mathrm{BH}}$ and radiation capacity is $0$, so the min is zero by nonnegativity of $S_{\mathrm{BH}}$.
proof idea
One-line wrapper. Rewrite the process radiation entropy via the Schmidt-purification identity, which identifies $P.S_{\mathrm{rad}}$ with the unitarity Page formula. Then apply pageCurveFromUnitarity_at_zero at the process black-hole entropy, using the process nonnegativity hypothesis. That upstream lemma unfolds the min-of-capacities definition and finishes with min_eq_right.
why it matters
Boundary condition at the start of evaporation: no radiation entropy before any Hawking quanta are emitted. Downstream, page_curve_derived_dynamical_prop_holds packages the full dynamical derivation and cites this fact as the $t = 0$ clause of the derived Page-curve property for the canonical process (alongside the $t = 1$ and Page-time peak clauses).
In the Track 3.C story this closes the initial endpoint of the triangle that Session 101 only wrote by hand. The module status is structural theorem (zero sorry). It does not yet derive the entropy readout from a microscopic Hamiltonian; that operator-level interface remains open per the upstream process-interface note.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.