PageCurveDynamicalProcess
plain-language theorem explainer
A Page-curve dynamical process packages initial black-hole entropy, a radiation-entropy path, and the Schmidt-purification hypothesis that radiation entropy always equals the min of bulk and radiation capacities. Gravity and quantum-information workers cite it as the structural carrier of unitarity-derived Page curves. It is a plain structure definition: no proof body, only field constraints.
Claim. A Page-curve dynamical process consists of an initial black-hole entropy $S_{\mathrm{BH}}\ge 0$, a radiation entropy function $S_{\mathrm{rad}}:\mathbb{R}\to\mathbb{R}$, and the Schmidt-purification hypothesis that for every evaporation fraction $t$, $S_{\mathrm{rad}}(t)=\min\bigl(S_{\mathrm{BH}}(1-t),\,S_{\mathrm{BH}}\,t\bigr)$ (the unitarity Page curve under linear capacity transfer).
background
Module 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]$: the fraction of entropy moved from bulk to radiation. Bulk capacity falls as $S_{\mathrm{BH}}(1-t)$; radiation capacity grows as $S_{\mathrm{BH}},t$. Their sum is the invariant $S_{\mathrm{BH}}$.
For a pure joint state on $H_{\mathrm{bulk}}\otimes H_{\mathrm{rad}}$, Schmidt's theorem forces equal reduced entropies, each at most $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$. Under maximal entanglement the radiation entropy saturates that bound, yielding $\min$ of the two linear capacities: the triangular Page curve peaking at $t=1/2$.
Session 101 only gave a kinematic piecewise-linear ansatz. This structure names the dynamical hypothesis explicitly so later theorems can inhabit it without committing to a full operator-level unitary model.
proof idea
No proof: this is a structure definition. Fields record initial entropy (with non-negativity), the radiation path, and the equality of that path to the unitarity Page curve at every $t$. Downstream, the canonical process fills the fields by setting radiation entropy equal to that min-of-capacities function and discharging the hypothesis by rfl.
why it matters
This is the data type for dynamical Page-curve claims in the module. The canonical process inhabits it by taking radiation entropy to be exactly the unitarity curve. The derived dynamical proposition asserts existence of such a process with the standard Page properties (starts and ends at zero, peaks at $S_{\mathrm{BH}}/2$ at $t=1/2$, non-negative on $[0,1]$). Phase-2 anti-monotonicity rewrites through the purification field and applies the corresponding property of the unitarity curve. The master certificate packages well-definedness and capacity invariants around the same carrier.
In Recognition Science terms it closes the gap between a hand-drawn triangular ansatz and a substrate principle: pure joint evolution plus linear capacity transfer forces the Page shape. The structure remains "structural" until full Hilbert-space unitary evolution is derived; when that lands, the hypothesis is automatic rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.