pageCurveStructuralCert
plain-language theorem explainer
Bundles the kinematic shape laws of the triangular Page curve (zero at ignition and full evaporation, peak equal to S_max at Page time, nonnegativity, identically zero after end) with the master-theorem Page-curve hypothesis witness. Gravity-track auditors cite it to discharge the structural certificate for Track 3.C. The body is a pure structure inhabitant: each field is filled by an already-proved lemma.
Claim. There is an inhabitant of the structural Page-curve certificate: the triangular radiation-entropy curve $S_{\mathrm{rad}}(S_{\max},t_{\mathrm{Page}},t)$ satisfies $S_{\mathrm{rad}}(0)=0$, $S_{\mathrm{rad}}(t_{\mathrm{Page}})=S_{\max}$ whenever $t_{\mathrm{Page}}>0$, $S_{\mathrm{rad}}(2 t_{\mathrm{Page}})=0$, is nonnegative for $S_{\max}\ge 0$ and $t_{\mathrm{Page}}>0$, vanishes for all $t>2 t_{\mathrm{Page}}$, and the master-theorem Page-curve hypothesis is witnessed by the structural derivation.
background
Track 3.C of the quantum-gravity master plan asks for a Page curve from ledger structure. This module ships only the kinematic content: a piecewise-linear triangular model of radiation entropy, not the full replica-wormhole or back-reaction dynamics.
The curve trianglePageCurve S_max t_Page t rises linearly from 0 to $S_{\max}$ on $[0,t_{\mathrm{Page}}]$, falls linearly back to 0 on $[t_{\mathrm{Page}},2 t_{\mathrm{Page}}]$, and is identically zero thereafter. Early time models thermal Hawking accumulation; the Page time is the half-evaporation peak; late time encodes the binding constraint of remaining black-hole entropy; full evaporation restores a pure global state.
The certificate structure packages the five shape laws (at zero, at peak, at end, nonnegativity, after-end zero) plus a PageCurveDerived witness that retires the corresponding hypothesis on the conditional master theorem rs_quantum_gravity_master_conditional.
proof idea
One-line structure constructor. Each field is assigned a named lemma already proved in the module: zero-at-start, peak-at-Page-time, zero-at-full-evaporation, nonnegativity, and identically-zero-after-end. The final field is the pre-built master-hypothesis witness that packages the structural derivation proposition and its proof. No new calculation occurs here.
why it matters
Closes the kinematic half of Track 3.C ("Page curve from ledger structure") in the quantum-gravity master plan. Downstream, pageCurveStructuralCert_inhabited records that the certificate type is nonempty, which is the one-statement structural form of the track.
The embedded master-hypothesis witness retires PageCurveDerived from the conditional master theorem, so gravity-track composition no longer carries an open Page-curve assumption at the structural layer. Full dynamical content (replica wormholes, quantum extremal surfaces, bulk back-reaction, unitary evolution on bulk ledger tensor Hawking radiation) remains outside this module and is estimated as multi-session work; this declaration only certifies the triangular shape that any such derivation must recover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.