pageCurveStructuralCert_inhabited
plain-language theorem explainer
The triangular Page-curve certificate is inhabited: radiation entropy starts at zero, peaks at S_max at the Page time, returns to zero at full evaporation (twice the Page time), stays non-negative, and vanishes thereafter. Quantum-gravity and RS master-theorem users cite this to discharge the kinematic Page-curve hypothesis input. The proof is a one-line term packaging the already-proved shape lemmas into the certificate structure.
Claim. The type of structural Page-curve certificates is nonempty. Equivalently, there is a witness that the triangular curve $S_{\mathrm{rad}}(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$; $S_{\mathrm{rad}}\ge 0$ for $S_{\max}\ge 0$; and $S_{\mathrm{rad}}(t)=0$ for all $t>2 t_{\mathrm{Page}}$.
background
Track 3.C of the RS quantum-gravity master plan asks for a Page curve from ledger structure. The full dynamical story (replica wormholes, quantum extremal surfaces, ledger-side back-reaction, unitary evolution on bulk ledger tensor Hawking radiation) is multi-session work. This module ships only the kinematic content: a piecewise-linear triangular shape that encodes the standard early-time rise, Page-time peak, late-time fall, and post-evaporation zero.
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 afterward. Physically this matches thermal Hawking accumulation before the Page time, the binding constraint of remaining black-hole entropy after it, and pure global state restoration at full evaporation.
PageCurveStructuralCert packages five universal shape facts (zero at start, peak value, zero at end, non-negativity, post-end vanishing). A sibling witness pageCurveDerivedWitness feeds the same content into the master-theorem hypothesis PageCurveDerived.
proof idea
One-line term proof. The certificate structure is inhabited by the concrete term pageCurveStructuralCert, which is already assembled from the sibling lemmas on the triangular curve (value at zero, at the Page time, at twice the Page time, non-negativity, and vanishing after full evaporation). Nonemptiness is immediate from that constructor.
why it matters
Closes the kinematic half of Track 3.C ("Page curve from ledger structure") with a 0-sorry structural theorem and supplies the master-theorem hypothesis witness that retires PageCurveDerived from the conditional quantum-gravity master theorem. Downstream, the certificate is the structural stand-in until the dynamical derivation (replica wormholes, QES, ledger back-reaction) is formalized. It does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; its role is gravity-side bookkeeping for unitary evaporation shape. The module doc flags the dynamical derivation as future multi-session work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.