pageCurveDynamicalCert
plain-language theorem explainer
Packages the dynamical Page-curve derivation into a single master certificate: radiation entropy equals min of bulk and radiation Hilbert capacities, with conserved capacity sum, forced peak at half-evaporation, and full return at complete evaporation. Gravity and quantum-info workers cite it as the closed witness that the triangular Page curve is forced by Schmidt purification rather than postulated. The body is a pure structure inhabitant wiring already-proved lemmas and the canonical process.
Claim. There is a dynamical Page-curve certificate asserting: for every initial black-hole entropy $S$ and evaporation fraction $t$, the unitarity Page curve equals $\min(S(1-t), St)$; bulk plus radiation capacity always equals $S$; phase-1 entropy tracks radiation capacity and phase-2 tracks bulk capacity; the peak at $t=1/2$ is $S/2$; entropy returns to zero at $t=1$; a canonical Schmidt-saturating process exists for every $S\ge 0$; and the master-theorem derived-Page-curve hypothesis is inhabited by the dynamical witness.
background
Gravity Track 3.C replaces the Session 101 kinematic triangular ansatz with a derivation from one substrate principle. Evaporation is parameterized by $t\in[0,1]$: the fraction of total entropy transferred from bulk to radiation. Bulk capacity falls as $S_{\mathrm{BH}}(1-t)$ while radiation capacity rises as $S_{\mathrm{BH}}t$. Their sum is conserved and equals $S_{\mathrm{BH}}$ at every $t$ (capacity-sum invariant).
Unitary evolution from a pure initial bulk state keeps the joint bulk$\otimes$radiation state pure. Schmidt purification then forces equal reduced entropies, each bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$. Under maximal Schmidt balance the radiation entropy saturates that bound, so it equals $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$. That minimum of two linear monotones is the triangular Page curve; the peak at $t=1/2$ is forced by symmetry.
The structure PageCurveDynamicalCert is the master certificate bundling curve definition, invariants, phase equalities, peak and return, a canonical process inhabitant, and the dynamical master-theorem witness that supersedes the kinematic one.
proof idea
Pure structure construction: each field is filled by a named prior result. curve_def is definitional reflexivity of the unitarity Page curve as the min of the two capacities. capacity_invariant is the ring identity capacity_sum_invariant. Phase-1 and phase-2 equalities, the half-time peak, and full return at $t=1$ are the corresponding pageCurveFromUnitarity_* theorems. canonical_inhabitant wraps canonicalProcess, the maximally saturating Schmidt-balanced ledger process whose radiation entropy is literally the unitarity curve. master_hypothesis_witness is pageCurveDerivedWitness_dynamical, the derivation-grade PageCurveDerived inhabitant for the gravity master theorem.
why it matters
This is the §7 master cert of the dynamical Page-curve module: the single object that records that the triangular shape is no longer an ansatz but min(bulkCap, radCap) under Schmidt purification. Downstream, pageCurveDynamicalCert_inhabited is the one-line Nonempty proof that simply packages this inhabitant, opening the one-statement dynamical Page-curve theorem section.
In the broader Recognition gravity track it closes the structural gap left by PageCurveStructural: Session 101 postulated the triangle; Track 3.C derives it from pure joint states and linear capacity transfer, with zero sorry and no RS-internal axiom (module status: structural theorem, closure 2026-05-22). It feeds the master-theorem hypothesis PageCurveDerived via the dynamical witness, so higher gravity assembly can cite a derivation-grade rather than kinematic input. The forced Page time $t=1/2$ and return to zero at full evaporation are the concrete unitarity signatures packaged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.