page_curve_derived_structural_prop
plain-language theorem explainer
The structural Page-curve proposition asserts that there exist positive peak radiation entropy and Page time for which the piecewise-linear triangular entropy curve starts at zero, peaks at the Page time, returns to zero at twice that time, and stays non-negative. Quantum-gravity workers on RS Track 3.C cite it as the kinematic content of the Page curve. It is a Prop definition packaging those shape conditions; existence is discharged by a companion theorem with concrete witnesses.
Claim. There exist real numbers $S_{\max} > 0$ and $t_{\mathrm{Page}} > 0$ such that the triangular Page curve with those parameters equals $0$ at $t = 0$, equals $S_{\max}$ at $t = t_{\mathrm{Page}}$, equals $0$ at $t = 2\, t_{\mathrm{Page}}$, and is non-negative for every real $t$.
background
Track 3.C of the RS quantum-gravity master plan asks for a Page curve from ledger structure. The full dynamical derivation (replica wormholes, quantum extremal surfaces, back-reaction, unitary bulk-plus-radiation evolution) is heavy; this module ships only the kinematic content: a fixed triangular shape for radiation entropy versus time.
The triangular Page curve is the piecewise-linear function that 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 (and for negative $t$). Early time models thermal Hawking accumulation; the Page time is half-evaporation, when radiation entropy equals remaining black-hole entropy; late time encodes purification as entanglement rearranges; full evaporation restores a pure global state.
Upstream, $t_{\mathrm{Page}}(M) = 5120\pi M^3$ is the RS-native Page time (standard Page factor times the $M^3$ scaling from integrating $dM/dt = -1/M^2$). The curve constructor itself is the local piecewise definition used in the proposition body.
proof idea
No proof: this is a bare Prop definition. The body is an existential package over two positive reals $S_{\max}$ and $t_{\mathrm{Page}}$, conjoining four shape facts about the triangular Page curve: value $0$ at the origin, value $S_{\max}$ at the Page time, value $0$ at twice the Page time, and global non-negativity. Companion lemmas on the curve (at zero, at peak, at end, non-negativity) discharge those conjuncts when the existence theorem is proved.
why it matters
This Prop is the hypothesis interface that the master-theorem witness expects. The companion theorem proves it holds (with concrete witnesses $S_{\max}=1$, $t_{\mathrm{Page}}=1$), and pageCurveDerivedWitness packages both into an inhabitant of PageCurveDerived. That witness retires the Page-curve hypothesis from the conditional quantum-gravity master theorem, closing the kinematic half of Track 3.C.
It does not replace the dynamical ledger derivation estimated at 6–10 sessions; it supplies the shape certificate the master plan needs so the conditional master theorem can drop one named hypothesis. In the RS gravity track this is the structural stand-in for the classic Page (1976) entropy curve, aligned with the RS-native Page-time scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.