PageCurveStructuralCert
plain-language theorem explainer
Certificate bundling the kinematic shape laws of the triangular Page curve (vanishes at t=0 and at full evaporation, peaks at S_max at the Page time, stays nonnegative, and is identically zero after 2 t_Page) plus a witness of the master-theorem PageCurveDerived hypothesis. Gravity-track and master-theorem consumers cite it to discharge Track 3.C structural obligations. As a structure there is no proof body; concrete inhabitants wire the sibling triangle lemmas and the derived witness.
Claim. A Page-curve structural certificate is a record of: (i) $P(S,t,0)=0$; (ii) $0<t\Rightarrow P(S,t,t)=S$; (iii) $0<t\Rightarrow P(S,t,2t)=0$; (iv) $S\ge 0$, $t>0\Rightarrow P(S,t,r)\ge 0$; (v) $0<t$ and $r>2t\Rightarrow P(S,t,r)=0$, where $P$ is the triangular Page curve with peak entropy $S$ and Page time $t$; together with (vi) an inhabitant of the master-theorem hypothesis that a dynamical Page curve has been derived.
background
Module Gravity.PageCurveStructural ships Track 3.C of the quantum-gravity master plan in kinematic form only: the triangular Page curve as a piecewise-linear function, not the full replica-wormhole / quantum-extremal-surface dynamics.
The curve $P(S_{\max}, t_{\mathrm{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 for $t>2 t_{\mathrm{Page}}$ (and for $t\le 0$ by convention). Early time models thermal Hawking accumulation; the Page time is half-evaporation with radiation entropy equal to remaining BH entropy; late time restores purity as information returns.
Upstream, PageCurveDerived is the master-theorem Track 3.C hypothesis interface: a Prop plus a proof it holds. The dynamical entropy evolution remains multi-session work; this module supplies the structural shape and a witness that retires the hypothesis from the conditional master theorem.
proof idea
Definitional structure, not a proved theorem: six fields, five of them universal statements about the triangular Page curve and one a term of type PageCurveDerived.
No tactics run at this declaration. Downstream, the canonical inhabitant fills the five curve fields by the sibling lemmas trianglePageCurve_at_zero, _at_peak, _at_end, _nonneg, and _after_end_zero, and supplies the master field via the structural PageCurveDerived witness built from page_curve_derived_structural_prop and its holding proof. Inhabitation is then a one-constructor Nonempty wrapper.
why it matters
Closes the kinematic half of Track 3.C ("Page curve from ledger structure") in the quantum-gravity master plan. The full dynamical derivation (unitary bulk-radiation evolution, replica wormholes, back-reaction) is still estimated heavy; this cert packages what is theorem-grade today so the conditional master theorem rs_quantum_gravity_master_conditional can drop the Page-curve hypothesis once the witness is plugged in.
Direct consumers are the canonical inhabitant pageCurveStructuralCert and the Nonempty theorem pageCurveStructuralCert_inhabited, which the module advertises as the Track 3.C one-statement structural form. In the broader RS gravity stack it sits under MasterTheorem and beside ILG action material, separating shape obligations from dynamics still open in PageCurveDerived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.