pageCurveFromUnitarity_phase1
plain-language theorem explainer
For evaporation fraction t in [0, 1/2], the unitarity Page curve equals radiation capacity S_BH · t (the ascending thermal-accumulation branch). Gravity and information theorists cite it when splitting the triangular Page curve into its two linear phases. The proof is a short min-identity: under t ≤ 1/2 one has S_BH · t ≤ S_BH · (1 − t), so min picks the radiation side.
Claim. Let $S_{\mathrm{BH}} \ge 0$ and $0 \le t \le 1/2$. Then the unitarity Page curve at evaporation fraction $t$ equals the radiation Hilbert-space capacity: $\min\bigl(S_{\mathrm{BH}}(1-t),\, S_{\mathrm{BH}} t\bigr) = S_{\mathrm{BH}} t$.
background
Track 3.C 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 linearly as $S_{\mathrm{BH}}(1-t)$; radiation capacity rises as $S_{\mathrm{BH}} t$.
Unitarity of the joint bulk–radiation evolution from a pure initial state forces the reduced entropies to coincide and to obey $S(\rho_{\mathrm{rad}}) \le \min(\log d_{\mathrm{bulk}}, \log d_{\mathrm{rad}})$. Under maximal Schmidt entanglement the bound saturates, so the radiation entropy is exactly $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$. That minimum is the dynamical Page curve.
Phase 1 is the radiation-bound ascent: while $t \le 1/2$ the radiation side is the smaller capacity, so entropy tracks thermal accumulation of Hawking quanta.
proof idea
Unfold the three definitions so the goal is $\min(S_{\mathrm{BH}}(1-t), S_{\mathrm{BH}} t) = S_{\mathrm{BH}} t$. Apply min_eq_right, which reduces to showing $S_{\mathrm{BH}} t \le S_{\mathrm{BH}}(1-t)$. From $t \le 1/2$ obtain $t \le 1-t$ by linear arithmetic, then multiply both sides by the nonnegative $S_{\mathrm{BH}}$.
why it matters
This is the Phase-1 half of the dynamical Page-curve identity. It feeds the certificate pageCurveDynamicalCert (field phase1_equals_radiation), the ascending monotonicity lemma on $[0,1/2]$, and the concrete radiation-entropy identification $S_{\mathrm{rad}}(t) = S_{\mathrm{BH}} t$ under Schmidt purification.
Together with the Phase-2 bulk-bound descent and the peak-at-half lemma, it closes the structural claim that the triangular Page curve is forced by unitarity plus linear capacity bookkeeping, not chosen by hand. In the Recognition gravity track this replaces the Session-101 kinematic ansatz with a derived min-of-capacities shape whose peak at $t=1/2$ is mandatory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.