canonicalProcess
plain-language theorem explainer
The canonical bulk–radiation ledger process: radiation entropy is exactly the unitarity Page curve min of bulk and radiation capacities. Anyone citing the dynamical Page-curve derivation uses this as the saturating witness. Construction is by filling the process structure with the unitarity curve and a reflexivity proof of Schmidt saturation.
Claim. Given initial black-hole entropy $S_{\mathrm{BH}} \ge 0$, there is a page-curve dynamical process with that entropy whose radiation entropy is $S_{\mathrm{rad}}(t) = \min\bigl(S_{\mathrm{BH}}(1-t),\, S_{\mathrm{BH}} t\bigr)$ and which saturates the Schmidt-purification bound at every evaporation fraction $t$.
background
Gravity 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]$: bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ while radiation capacity grows as $S_{\mathrm{BH}} t$. A pure joint state on $H_{\mathrm{bulk}} \otimes H_{\mathrm{rad}}$ forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}}, \log d_{\mathrm{rad}})$.
A page-curve dynamical process packages initial entropy $S_{\mathrm{BH}} \ge 0$, a radiation entropy function $S_{\mathrm{rad}}$, and the Schmidt-purification hypothesis that $S_{\mathrm{rad}}(t)$ equals that min-of-capacities bound at every $t$. The unitarity Page curve is defined as exactly $\mathrm{pageCurveFromUnitarity}(S_{\mathrm{BH}}, t) = \min(\mathrm{bulkCapacity}, \mathrm{radiationCapacity})$: the unique saturation of the entropy bound under linear capacity transfer.
proof idea
Definitional constructor, not a tactic proof. Feed $S_{\mathrm{BH}}$ and its non-negativity into the process structure; set radiation entropy to the partial application of the unitarity Page curve at that $S_{\mathrm{BH}}$; discharge Schmidt purification by reflexivity, since that curve is defined to be the min-of-capacities bound.
why it matters
This is the maximally saturating Schmidt-balanced evolution used as the concrete witness for the dynamical Page-curve claim. Downstream, page_curve_derived_dynamical_prop_holds instantiates it at $S_{\mathrm{BH}} = 1$ to prove the derived dynamical property (boundary values and Page-time peak). The certificate pageCurveDynamicalCert packages the same unitarity curve's phase equalities and half-time peak.
In the module narrative this closes the gap left by the kinematic triangular ansatz of Session 101: the triangle, including the forced peak at $t = 1/2$ and return to zero, emerges from purity plus linear capacity transfer rather than being drawn by hand. It sits in the gravity track as the recognition-ledger realization of unitary black-hole evaporation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.