PageCurveDynamicalCert
plain-language theorem explainer
Packages the dynamical Page-curve certificate: radiation entropy equals min of bulk and radiation capacities, with the capacity sum fixed at the initial black-hole entropy S. Anyone citing the derived triangular Page curve (peak S/2 at half-evaporation, return to zero at full evaporation) points here. The structure is a pure interface; the concrete inhabitant fills each field by rfl or named capacity lemmas.
Claim. A certificate bundling: (i) the unitarity Page curve equals $\min(\mathrm{bulk\,capacity}(S,t),\mathrm{rad\,capacity}(S,t))$; (ii) those capacities sum to $S$; (iii) for $0\le t\le 1/2$ the curve equals radiation capacity, and for $1/2\le t\le 1$ it equals bulk capacity; (iv) value $S/2$ at $t=1/2$ and $0$ at $t=1$ (when $S\ge 0$); (v) a nonempty dynamical process for each $S\ge 0$; (vi) a witness that the master-theorem Page-curve hypothesis holds.
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 total entropy transferred from bulk to radiation. Bulk capacity falls as $S(1-t)$; radiation capacity rises as $St$.
Unitarity keeps the joint bulk$\otimes$radiation state pure, so Schmidt's theorem forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$. Under maximal Schmidt balance the radiation entropy saturates that bound, yielding $\min$ of the two linear capacities: the triangular Page curve with forced peak at $t=1/2$.
PageCurveDynamicalProcess is the process structure: initial $S_{BH}\ge 0$, a radiation-entropy function, and the Schmidt-purification hypothesis that $S_{\mathrm{rad}}(t)$ equals the min-of-capacities bound at every $t$. This certificate aggregates the algebraic identities and the master-theorem witness built on that process.
proof idea
No proof body: this is a structure (bundle of named fields). Downstream pageCurveDynamicalCert inhabits it fieldwise: curve_def by rfl against the definition of pageCurveFromUnitarity; capacity_invariant by capacity_sum_invariant; phase equalities by pageCurveFromUnitarity_phase1 and _phase2; peak and full-evaporation return by the corresponding half/one lemmas; process nonemptiness and PageCurveDerived by the recognition-tick transfer witness already constructed in the module. pageCurveDynamicalCert_inhabited is then just ⟨pageCurveDynamicalCert⟩.
why it matters
Closes the Session-101 gap: the triangular Page curve is no longer a kinematic ansatz but a derived min-of-capacities identity under Schmidt purification. The structure is the master cert (§7) that feeds pageCurveDynamicalCert and the nonempty theorem, and supplies Gravity.MasterTheorem.PageCurveDerived so the conditional master theorem can discharge its Page-curve hypothesis.
In the RS gravity track this is the dynamical half of black-hole information return: unitarity plus ledger capacities force information back to zero at full evaporation, with the Page time fixed at half-evaporation. It sits downstream of the structural Page-curve module and upstream of the one-statement dynamical Page-curve theorem that follows the inhabited cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.