page_curve_one_statement
plain-language theorem explainer
The triangular Page curve of radiation entropy is theorem-grade in its kinematics: zero at t=0, peak S at the Page time, zero again at full evaporation 2t, and non-negative for S≥0. The same certificate inhabits the master-theorem hypothesis PageCurveDerived. Gravity and QG workers cite it as the closed structural half of Track 3.C. The proof is a five-conjunct term packing four shape lemmas plus the structural witness.
Claim. For the piecewise-linear triangular Page curve $P(S,t,r)$ of peak entropy $S$ and Page time $t$: $P(S,t,0)=0$ for all $S,t$; if $t>0$ then $P(S,t,t)=S$ and $P(S,t,2t)=0$; if $S\ge 0$ and $t>0$ then $P(S,t,r)\ge 0$ for all $r$; and the master-theorem structure asserting a derived Page curve is inhabited (nonempty).
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, ledger-side back-reaction, unitary evolution on bulk ledger tensor Hawking radiation) is multi-session work. This module ships only the kinematic content: a canonical triangular shape for radiation entropy versus time.
The structural 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}},2t_{\mathrm{Page}}]$, and is identically zero after full evaporation (and for negative $t$ by convention). Early time matches thermal Hawking accumulation; the Page time is half-evaporation, where radiation entropy equals remaining black-hole thermodynamic entropy; late time replaces BH-radiation entanglement by radiation-radiation entanglement until purity is restored.
Upstream, PageCurveDerived is the master-theorem hypothesis structure whose field is a Prop together with a proof it holds. The structural witness fills that structure with the kinematic property bundle proved in this module, so the conditional master theorem no longer treats Page-curve existence as an open external assumption.
proof idea
Term-mode five-fold conjunction. The first four conjuncts are exactly the named shape lemmas: value $0$ at time $0$; value $S$ at the Page time (under $t>0$); value $0$ at $2t$ (under $t>0$); and non-negativity when $S\ge 0$ and $t>0$. The fifth conjunct is Nonempty PageCurveDerived, discharged by packaging the structural witness as an explicit inhabitant. No new case analysis appears here; the heavy unfolding of the piecewise definition lives in those four lemmas.
why it matters
Closes the structural half of Track 3.C ("Page curve from ledger structure") with zero sorry and no RS-internal axiom. The doc-comment frames it as the one-statement kinematic certificate: starts at zero, peaks at $S_{\max}$ at $t_{\mathrm{Page}}$, returns to zero at $2t_{\mathrm{Page}}$, stays non-negative, and vanishes after full evaporation, while inhabiting PageCurveDerived.
That inhabitant retires the Page-curve hypothesis from the conditional quantum-gravity master theorem: once the structural witness is in hand, master-level statements no longer need an external open assumption for the curve's existence in kinematic form. Downstream use count is currently zero in the graph, so this is a leaf cert rather than an intermediate lemma.
The dynamical derivation from RS first principles (replica wormholes, QES comparison, ledger-side evaporation dynamics) remains explicitly future work. Page-time $M^3$ scaling is already closed elsewhere; entropy evolution is not. This declaration therefore marks a clean split between proved kinematics and open dynamics inside the gravity track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.