trianglePageCurve_at_end
plain-language theorem explainer
At full evaporation time $2 t_{\mathrm{Page}}$, the structural radiation entropy vanishes: $S_{\mathrm{rad}}(2 t_{\mathrm{Page}})=0$. Anyone citing the kinematic Page-curve shape (Track 3.C) needs this endpoint. The proof unfolds the piecewise definition, rules out the early phases by positivity of $t_{\mathrm{Page}}$, then finishes by field simplification and ring.
Claim. For all real $S_{\max}$ and $t_{\mathrm{Page}}>0$, the triangular Page curve satisfies $S_{\mathrm{rad}}(S_{\max}, t_{\mathrm{Page}}; 2 t_{\mathrm{Page}})=0$. That is, radiation entropy returns to zero exactly at full evaporation.
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 full replica-wormhole / QES derivation.
The structural curve $S_{\mathrm{rad}}(S_{\max}, t_{\mathrm{Page}}; t)$ is defined by three phases. For $0\le t\le t_{\mathrm{Page}}$ it rises linearly from $0$ to $S_{\max}$; for $t_{\mathrm{Page}}\le t\le 2 t_{\mathrm{Page}}$ it falls linearly back to $0$; thereafter it is identically zero. Negative times are 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$ is the RS-native Page time from integrating $dM/dt=-1/M^2$. Entropy elsewhere in the stack (configuration defect, horizon microstate log) motivates why a pure final state should carry zero radiation entropy, but this lemma is purely about the piecewise formula.
proof idea
Unfold the piecewise definition of the triangular curve. From $t_{\mathrm{Page}}>0$ obtain $2 t_{\mathrm{Page}}\not\le 0$ and $2 t_{\mathrm{Page}}\not\le t_{\mathrm{Page}}$ by push_neg and linarith, so the evaluation lands in the descent branch $S_{\max}-(S_{\max}/t_{\mathrm{Page}})(t-t_{\mathrm{Page}})$. Also record $t_{\mathrm{Page}}\ne 0$. simp selects that branch; field_simp clears the division; ring reduces the expression at $t=2 t_{\mathrm{Page}}$ to $0$.
why it matters
This is the full-evaporation endpoint of the structural Page curve: information has returned and radiation entropy is again zero, matching unitary restoration of a pure global state. It is one of the five shape facts packaged into pageCurveStructuralCert and is invoked directly by page_curve_derived_structural_prop_holds (with unit parameters) and by the Track 3.C one-statement theorem, which asserts among other clauses that $\forall S,t>0$, the curve at $2t$ is zero and that the master-theorem hypothesis PageCurveDerived is inhabited.
Within Recognition Science this closes the kinematic half of Gravity Track 3.C. The dynamical derivation (replica wormholes, quantum extremal surfaces, ledger-side back-reaction on BulkLedger ⊗ HawkingRadiation) remains future work estimated at several sessions; the structural witness is what the master theorem consumes today.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.