trianglePageCurve
plain-language theorem explainer
Canonical triangular Page curve: radiation entropy rises linearly from 0 to peak S_max by the Page time, falls linearly back to 0 by full evaporation at twice that time, and is zero outside. Gravity and QG workers cite it as the kinematic skeleton of Track 3.C. The body is a four-branch piecewise definition with no proof obligations.
Claim. Define the triangular Page curve $S_{\mathrm{rad}}(S_{\max}, t_{\mathrm{Page}}, t)$ by $0$ if $t \le 0$; $(S_{\max}/t_{\mathrm{Page}})\, t$ if $0 < t \le t_{\mathrm{Page}}$; $S_{\max} - (S_{\max}/t_{\mathrm{Page}})(t - t_{\mathrm{Page}})$ if $t_{\mathrm{Page}} < t \le 2 t_{\mathrm{Page}}$; and $0$ if $t > 2 t_{\mathrm{Page}}$. Here $S_{\max}$ is peak radiation entropy and $t_{\mathrm{Page}}$ is the half-evaporation time.
background
Track 3.C of the quantum-gravity master plan asks for a Page curve from ledger structure. The full dynamical story (replica wormholes, quantum extremal surfaces, back-reaction on BulkLedger ⊗ HawkingRadiation) is multi-session work. This module ships only the kinematic content: a fixed triangular shape and its elementary shape lemmas, plus a witness for the master-theorem hypothesis.
The classical Page picture is that early Hawking radiation looks thermal, so radiation entropy climbs; at the Page time half the black hole is gone and radiation entropy equals remaining BH entropy; thereafter entanglement rearranges and radiation entropy falls, hitting zero at full evaporation when the global state is pure again. The RS-native Page time scales as $t_{\mathrm{Page}}(M) = 5120\pi M^3$ from integrating $dM/dt = -1/M^2$.
This definition is the pure shape function of those three phases (plus a zero convention for negative time). It does not encode mass loss, temperature, or ledger dynamics; those enter only when the shape is later tied to physical parameters.
proof idea
Pure definition, not a proved theorem. Four mutually exclusive real branches on the time argument: non-positive time maps to 0; the first Page interval is the ray of slope $S_{\max}/t_{\mathrm{Page}}$; the second Page interval is the descending ray of opposite slope that hits 0 at $2 t_{\mathrm{Page}}$; everything later is 0. Downstream shape lemmas simply unfold this definition and discharge the branch guards by linarith / push_neg.
why it matters
This is the carrier object for Gravity Track 3.C structural form. Every shape lemma in the module (trianglePageCurve_at_zero, _at_peak, _at_end, _after_end_zero, _neg_zero, non-negativity, phase monotonicities) is stated about it. The existential package page_curve_derived_structural_prop quantifies over positive $S_{\max}$ and $t_{\mathrm{Page}}$ and asserts the key point values and non-negativity of this function; that package, once proved, inhabits PageCurveDerived via pageCurveDerivedWitness and thereby retires the Page-curve hypothesis from the conditional master theorem rs_quantum_gravity_master_conditional.
The one-statement theorem page_curve_one_statement packages the same kinematic facts plus the nonempty witness. What remains open is the dynamical derivation from RS substrate first principles (replica wormholes, QES, ledger-side back-reaction), explicitly deferred by the module header as future multi-session work. The triangular skeleton itself is closed (0 sorry, 0 RS-internal axiom).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.