trianglePageCurve_at_peak
plain-language theorem explainer
At the Page time the structural radiation-entropy curve equals its peak value S_max. Anyone citing the kinematic Page-curve shape (Track 3.C) uses this identity. The proof unfolds the piecewise definition, discards the t≤0 branch by positivity of t_Page, and simplifies the linear ascent branch to S_max.
Claim. For all real $S_{\max}$ and $t_{\mathrm{Page}}$ with $t_{\mathrm{Page}} > 0$, the triangular Page curve evaluated at the Page time equals the peak: $S_{\mathrm{rad}}(t_{\mathrm{Page}}) = S_{\max}$.
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 curve that stands in for radiation entropy during black-hole evaporation, together with a master-theorem hypothesis witness. Full dynamical derivation (replica wormholes, QES, ledger back-reaction) is deferred.
The structural curve trianglePageCurve S_max t_Page t has three phases on $t \ge 0$: linear ascent from $0$ to $S_{\max}$ on $[0, t_{\mathrm{Page}}]$, linear descent back to $0$ on $[t_{\mathrm{Page}}, 2 t_{\mathrm{Page}}]$, and identically zero thereafter. Negative $t$ is zero by convention. Here $S_{\max}$ is the peak radiation entropy and $t_{\mathrm{Page}}$ is the half-evaporation (Page) time; upstream, $t_{\mathrm{Page}}(M) = 5120\pi M^3$ in RS-native units.
Physically, $t = t_{\mathrm{Page}}$ is when half the black hole has evaporated: radiation entropy reaches its maximum and equals the remaining BH thermodynamic entropy, before late-time purification drives it back down.
proof idea
Term-mode proof by unfolding the piecewise definition. From $0 < t_{\mathrm{Page}}$ one gets $\neg(t_{\mathrm{Page}} \le 0)$ and $t_{\mathrm{Page}} \ne 0$. The first branch is therefore skipped; simp lands in the ascent branch $(S_{\max}/t_{\mathrm{Page}})\cdot t$ at $t = t_{\mathrm{Page}}$. A single field_simp cancels the ratio and yields $S_{\max}$.
why it matters
This is one of the three vertex identities that pin the triangular Page curve: zero at $t=0$, peak $S_{\max}$ at $t_{\mathrm{Page}}$, zero at full evaporation $2 t_{\mathrm{Page}}$. Downstream it is wired into pageCurveStructuralCert (field curve_at_peak), into the existential witness page_curve_derived_structural_prop_holds (with unit parameters), and into the Track 3.C one-statement page_curve_one_statement, which packages start/peak/end/nonnegativity plus Nonempty PageCurveDerived for the gravity master theorem.
It closes the kinematic half of Track 3.C ("Page curve from ledger structure"). The dynamical half — deriving the triangle from RS substrate, replica wormholes, and ledger-side back-reaction — remains explicitly open multi-session work. No forcing-chain landmark (T0–T8) is invoked; the result is pure shape calculus on the structural curve.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.