trianglePageCurve_neg_zero
plain-language theorem explainer
For negative times the structural Page curve vanishes by convention: radiation entropy is zero before evaporation starts. Anyone citing the kinematic Page-curve shape in Track 3.C needs this boundary clause. The proof unfolds the piecewise definition and discharges the first branch from t < 0 implying t ≤ 0.
Claim. For all real $S_{\max}$, $t_{\mathrm{Page}}$, and $t$ with $t < 0$, the triangular Page-curve function 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 its shape lemmas and a master-theorem hypothesis witness. The full replica-wormhole / QES derivation remains out of scope.
The structural curve is defined by three phases on $[0,\infty)$ plus a negative-time convention. Phase 1 ($0 \le t \le t_{\mathrm{Page}}$) is linear ascent from $0$ to $S_{\max}$; phase 2 ($t_{\mathrm{Page}} \le t \le 2 t_{\mathrm{Page}}$) is linear descent back to $0$; phase 3 ($t > 2 t_{\mathrm{Page}}$) is identically zero. For $t \le 0$ the value is set to $0$ by convention (no radiation before the start). Here $S_{\max}$ is 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$.
Sibling lemmas pin the values at $0$, at the peak, at the end, and after the end, plus non-negativity and unimodality under mild sign hypotheses on $S_{\max}$ and $t_{\mathrm{Page}}$.
proof idea
One short tactic proof. Unfold the piecewise definition of the triangular Page curve. The first branch returns $0$ whenever $t \le 0$. From the hypothesis $t < 0$, le_of_lt supplies $t \le 0$, and simp selects that branch.
why it matters
Closes the negative-time boundary clause of the structural Page curve required by Track 3.C ("Page curve from ledger structure"). Without it the piecewise definition is incomplete on $\mathbb{R}$, and later non-negativity / unimodality statements would need ad-hoc case splits. The module status is structural theorem (0 sorry, 0 RS-internal axiom): this lemma is part of that kinematic package and feeds the master-theorem hypothesis witness for the gravity track. It does not itself derive the Page curve from ledger dynamics or replica wormholes; those remain the heavy open sessions estimated in the master plan. No downstream consumers are wired yet; the immediate audience is the sibling shape lemmas and the structural witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.