S_rad_mono_phase1
plain-language theorem explainer
On the first half of evaporation, radiation entropy is nondecreasing: if $0\le t_1\le t_2\le 1/2$ then $S_{\mathrm{rad}}(t_1)\le S_{\mathrm{rad}}(t_2)$. Cited by anyone tracking the ascending leg of the dynamical Page curve under Schmidt purification. Proof is a two-line rewrite to the unitarity min-curve, then the phase-1 mono lemma.
Claim. Let $P$ be a Schmidt-purified Page-curve ledger with nonnegative black-hole entropy. For real evaporation fractions satisfying $0 \le t_1 \le t_2 \le 1/2$, the radiation entropy is monotone: $S_{\mathrm{rad}}(t_1) \le S_{\mathrm{rad}}(t_2)$.
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 transferred from bulk to radiation. Bulk capacity falls as $S_{BH}(1-t)$; radiation capacity grows as $S_{BH},t$.
Unitarity keeps the joint bulk$\otimes$radiation state pure, so Schmidt's theorem forces $S(\rho_{\mathrm{bulk}})=S(\rho_{\mathrm{rad}})$ and both are bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$. Under maximal Schmidt balance the radiation entropy saturates that bound, equaling $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$. That min-of-two-linear bounds is the triangular Page curve, with a forced peak at $t=1/2$.
Phase 1 is the interval $[0,1/2]$, where radiation capacity is the active (smaller) bound and is increasing. The upstream lemma pageCurveFromUnitarity_mono_phase1 already records ascending monotonicity for that abstract min-curve.
proof idea
Term-mode, two steps. First rewrite both sides of the goal with the ledger's Schmidt-purification identity, replacing $P.S_{\mathrm{rad}}$ by the unitarity Page curve pageCurveFromUnitarity at the same $S_{BH}$ and $t$. Then apply pageCurveFromUnitarity_mono_phase1 with nonnegativity of $P.S_{BH}$ and the three interval hypotheses $0\le t_1\le t_2\le 1/2$. No further case splits.
why it matters
Closes the ascending half of the dynamical Page curve for the concrete radiation-entropy field on a Schmidt-purified ledger. Session 101 only had a kinematic triangular ansatz; this module forces the triangle from purity plus linear capacities, and the phase-1 mono statement is the first half of that shape (ascent to the $t=1/2$ peak). The companion phase-2 anti-monotonicity (descent) sits immediately below in the file. No downstream consumers are wired yet (used_by empty), so the lemma is presently a leaf of the Track 3.C structural closure rather than an intermediate for a larger named theorem. It does not touch the RS forcing chain T0–T8 or the RCL; it lives entirely in the gravity/Page-curve track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.