pageCurveFromUnitarity_phase2
plain-language theorem explainer
For evaporation fraction t at least one half, the unitarity Page curve equals remaining bulk capacity S_BH(1-t). Anyone citing the dynamical triangular Page curve in the purifying half of evaporation needs this identity. The proof unfolds the min definition and uses t ≥ 1/2 plus nonnegativity of S_BH to pick the left branch.
Claim. Let $S_{\mathrm{BH}}\ge 0$ and $t\in[1/2,1]$. Then the unitarity Page curve $\min\bigl(S_{\mathrm{BH}}(1-t),\,S_{\mathrm{BH}} t\bigr)$ equals the bulk capacity $S_{\mathrm{BH}}(1-t)$.
background
Track 3.C derives the triangular Page curve from Schmidt purification on a pure joint bulk⊗radiation state, rather than postulating a piecewise-linear ansatz. Evaporation is parameterized by $t\in[0,1]$: the fraction of total entropy transferred from bulk to radiation.
Bulk capacity is the linear decrease $S_{\mathrm{BH}}(1-t)$; radiation capacity is the linear growth $S_{\mathrm{BH}} t$. The Page curve is defined as their minimum: the unique saturation of the entropy bound forced by purity of the joint state (Schmidt: $S(\rho_{\mathrm{bulk}})=S(\rho_{\mathrm{rad}})\le\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$).
Phase 1 ($t\le 1/2$) is radiation-bound ascent; phase 2 ($t\ge 1/2$) is bulk-bound descent, the information-purifying regime in which remaining bulk Hilbert-space dimension is the tighter ceiling.
proof idea
Unfold the three definitions so the goal is $\min(S_{\mathrm{BH}}(1-t), S_{\mathrm{BH}} t)=S_{\mathrm{BH}}(1-t)$. Apply min_eq_left, reducing to $S_{\mathrm{BH}}(1-t)\le S_{\mathrm{BH}} t$. From $t\ge 1/2$, linarith gives $1-t\le t$; multiply on the left by $S_{\mathrm{BH}}\ge 0$ via mul_le_mul_of_nonneg_left. The unused hypothesis $t\le 1$ is present only to mark the phase interval.
why it matters
This is the phase-2 half of the dynamical Page-curve identity. It is wired into pageCurveDynamicalCert as phase2_equals_bulk, the certificate that the derived curve matches bulk capacity after the Page time. Downstream, S_rad_phase2 rewrites physical radiation entropy via Schmidt purification plus this lemma, and pageCurveFromUnitarity_anti_mono_phase2 uses it to prove descending anti-monotonicity on $[1/2,1]$.
Together with the phase-1 dual and the peak-at-half lemma, it closes the structural claim that the triangular shape (rise, peak forced at $t=1/2$, return to zero) emerges from unitarity and linear capacity transfer alone. No RS-internal axiom or sorry remains in this module (closure 2026-05-22).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.