pageCurveFromUnitarity_at_zero
plain-language theorem explainer
At the start of evaporation the unitarity-derived Page curve vanishes: radiation entropy is zero when no Hawking quanta have been emitted. Gravity and information theorists cite this as the initial boundary condition of the triangular Page curve. The proof unfolds the min-of-capacities definition, applies the bulk and radiation evaluations at t = 0, and uses nonnegativity of black-hole entropy to select the radiation side of the min.
Claim. For any black-hole entropy $S_{\mathrm{BH}} \ge 0$, the unitarity Page curve at evaporation fraction $t = 0$ equals zero: $\min\bigl(S_{\mathrm{BH}}\cdot(1-0),\, S_{\mathrm{BH}}\cdot 0\bigr) = 0$.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt purification on a pure bulk ⊗ radiation joint state, rather than postulating it as a kinematic ansatz.
Evaporation is parameterized by $t \in [0,1]$. Bulk capacity falls linearly as $S_{\mathrm{BH}}\cdot(1-t)$; radiation capacity rises as $S_{\mathrm{BH}}\cdot t$. The Page curve is defined as the min of those two capacities: the unique saturation of the entropy bound forced by purity of the joint state (Schmidt balance).
Upstream, bulkCapacity at $t=0$ equals $S_{\mathrm{BH}}$, and radiationCapacity at $t=0$ equals $0$. The definition packages $S_{\mathrm{rad}}(t)=\min(\mathrm{bulk},\mathrm{rad})$.
proof idea
Short tactic proof in three steps. Unfold the unitarity Page-curve definition to expose $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$. Rewrite with the two simp lemmas that evaluate capacities at $t=0$, obtaining $\min(S_{\mathrm{BH}},0)$. Finish by min_eq_right using the hypothesis $0 \le S_{\mathrm{BH}}$.
why it matters
Feeds the dynamical Page-curve one-statement, which packages the full triangular shape: min form, capacity-sum invariant, vanishing at both endpoints, and peak at Page time $t=1/2$ with value $S_{\mathrm{BH}}/2$. Also used by the radiation-entropy-at-zero lemma for a Schmidt-purified process, which rewrites the readout through this boundary fact.
This is the initial boundary condition of Track 3.C's dynamical recipe: at $t=0$ the hole has not evaporated, so radiation entropy must start at zero. Module status is structural theorem (0 sorry). Deriving the entropy readout from a specific microscopic Hamiltonian or recognition update remains open at the operator-interface layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.