trianglePageCurve_after_end_zero
plain-language theorem explainer
After the Page time doubled, the structural radiation-entropy curve is identically zero: full evaporation has returned all information. Anyone assembling the kinematic Page-curve certificate cites this endpoint. The proof unfolds the piecewise definition and discharges the three earlier branches by linear arithmetic on the hypothesis t > 2 t_Page.
Claim. For real parameters $S_{\max}$, $t_{\mathrm{Page}}$, $t$ with $0 < t_{\mathrm{Page}}$ and $t > 2\, t_{\mathrm{Page}}$, the triangular Page curve evaluates to zero: $S_{\mathrm{rad}}(t) = 0$.
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 radiation entropy $S_{\mathrm{rad}}(t)$ during black-hole evaporation, together with a master-theorem hypothesis witness. The full replica-wormhole / quantum-extremal-surface derivation remains out of scope.
The structural curve trianglePageCurve S_max t_Page t has three phases on $[0,\infty)$: 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 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>2 t_{\mathrm{Page}}$ is full evaporation: BH-radiation entanglement has been replaced by radiation-radiation entanglement and the global state is pure again, so radiation entropy vanishes.
proof idea
One short tactic proof. Unfold the piecewise definition of the triangular curve. From $0<t_{\mathrm{Page}}$ and $t>2 t_{\mathrm{Page}}$, linear arithmetic yields the three negated guards $\neg(t\le 0)$, $\neg(t\le t_{\mathrm{Page}})$, and $\neg(t\le 2 t_{\mathrm{Page}})$. Simplification then selects the final else 0 branch. No external lemmas beyond linarith/simp are required.
why it matters
This is the Phase-3 endpoint of the structural Page curve: after full evaporation, $S_{\mathrm{rad}}=0$. It is wired directly into pageCurveStructuralCert as the field curve_after_end_zero, alongside the zero, peak, end, and nonnegativity facts. That certificate is the master-theorem hypothesis witness for Track 3.C ("Page curve from ledger structure").
In the Recognition framework the triangular shape encodes the ledger story of evaporation: early thermal accumulation, Page-time maximum when half the hole is gone, late-time purification as entanglement reorganizes, and final purity at $t=2 t_{\mathrm{Page}}$. Closing the after-end identity completes the kinematic skeleton; dynamics (back-reaction, bulk-ledger unitarity, replica wormholes) remain the heavy open work estimated at 6-10 sessions in the master plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.