trianglePageCurve_nonneg
plain-language theorem explainer
The triangular Page curve stays non-negative for every real time, given a non-negative peak entropy and a positive Page time. Gravity and QG workers cite it when assembling the kinematic Page-curve certificate and the Track 3.C one-statement. The proof is a four-way case split on the piecewise definition, with non-negativity of the linear pieces settled by division and multiplication inequalities plus a short linarith bound on the descent segment.
Claim. For all real $S_{\max}$, $t_{\mathrm{Page}}$, and $t$, if $0 \le S_{\max}$ and $0 < t_{\mathrm{Page}}$, then the triangular Page curve $S_{\mathrm{rad}}(t)$ (linear ascent $0\to S_{\max}$ on $[0,t_{\mathrm{Page}}]$, linear descent $S_{\max}\to 0$ on $[t_{\mathrm{Page}},2t_{\mathrm{Page}}]$, zero outside) satisfies $0 \le S_{\mathrm{rad}}(t)$.
background
Track 3.C of the quantum-gravity master plan asks for a Page curve from ledger structure. This module ships only the kinematic content: a piecewise-linear triangular shape that stands in for the radiation entropy during black-hole evaporation, together with the shape lemmas needed as a master-theorem hypothesis witness. The full dynamical story (replica wormholes, quantum extremal surfaces, ledger back-reaction) is deferred.
The structural curve is defined by cases on time $t$. For $t\le 0$ it is zero by convention. On the ascent phase $0\le t\le t_{\mathrm{Page}}$ it equals $(S_{\max}/t_{\mathrm{Page}}),t$. On the descent phase $t_{\mathrm{Page}}\le t\le 2t_{\mathrm{Page}}$ it equals $S_{\max}-(S_{\max}/t_{\mathrm{Page}})(t-t_{\mathrm{Page}})$. After full evaporation it is identically zero. Here $S_{\max}$ is the peak radiation entropy and $t_{\mathrm{Page}}$ is the half-evaporation (Page) time; an upstream RS-native formula gives $t_{\mathrm{Page}}(M)=5120\pi M^3$ from integrating $dM/dt=-1/M^2$, but this lemma treats $t_{\mathrm{Page}}$ as an arbitrary positive real parameter.
proof idea
Unfold the piecewise definition and case-split on the four regimes.
- If $t\le 0$, the value is definitionally $0$.
- If $0<t\le t_{\mathrm{Page}}$, the value is $(S_{\max}/t_{\mathrm{Page}}),t$. The slope $S_{\max}/t_{\mathrm{Page}}$ is non-negative by
div_nonnegfrom the two hypotheses, $t\ge 0$ follows by pushing the negated first case, and the product is non-negative. - If $t_{\mathrm{Page}}<t\le 2t_{\mathrm{Page}}$, the value is $S_{\max}-(S_{\max}/t_{\mathrm{Page}})(t-t_{\mathrm{Page}})$. Bound the subtracted term: $t-t_{\mathrm{Page}}\le t_{\mathrm{Page}}$ by
linarith, multiply by the non-negative slope, simplify $(S_{\max}/t_{\mathrm{Page}})\cdot t_{\mathrm{Page}}=S_{\max}$ byfield_simp, thenlinarithyields non-negativity of the difference. - If $t>2t_{\mathrm{Page}}$, the value is again definitionally $0$.
why it matters
Non-negativity is one of the five kinematic shape facts that make the triangular Page curve theorem-grade. It is wired directly into pageCurveStructuralCert as the curve_nonneg field, and it appears as the fourth conjunct of page_curve_one_statement (the Track 3.C one-statement): for all $S,t,r$ with $0\le S$ and $0<t$, the curve at $r$ is non-negative. The same lemma is used when inhabiting page_curve_derived_structural_prop for the master-theorem witness.
In the Recognition framework this closes the structural half of Gravity Track 3.C ("Page curve from ledger structure"). The triangular shape encodes the standard early-time thermal rise, peak at Page time equal to remaining BH entropy, late-time decline under the BH entropy bound, and return to zero at full evaporation. What remains open is the dynamical derivation from RS substrate first principles (replica wormholes, QES, ledger-side back-reaction), estimated as multi-session work beyond this kinematic certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.