trianglePageCurve_at_zero
plain-language theorem explainer
The structural (triangular) Page curve vanishes at time zero for any peak entropy and Page time: no radiation has been emitted yet. Gravity and QG workers cite it as the early-time boundary condition of Track 3.C. The proof is a one-step unfold-and-simp against the piecewise definition's first branch.
Claim. For all real $S_{\max}$ and $t_{\mathrm{Page}}$, the triangular Page-curve function satisfies $S_{\mathrm{rad}}(0)=0$, i.e. $\mathrm{trianglePageCurve}(S_{\max},t_{\mathrm{Page}},0)=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)$, not the full replica-wormhole or QES dynamics.
The structural curve 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 set to 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 (standard Page factor times the $M^3$ scaling from $\mathrm{d}M/\mathrm{d}t=-1/M^2$). Entropy in the foundation layer is total defect, so zero defect is the minimum-entropy state; the present lemma is the radiation-side analogue at $t=0$.
proof idea
One-line unfold-and-simp proof. Unfolding the piecewise definition exposes the leading branch if t ≤ 0 then 0. Instantiating at $t=0$ makes that guard true, so simp reduces the whole expression to $0$. No arithmetic lemmas or positivity hypotheses are required.
why it matters
This is the early-time anchor of the structural Page curve. It is wired into pageCurveStructuralCert as curve_at_zero, and is the first conjunct discharged by page_curve_derived_structural_prop_holds (with unit parameters) and by the Track 3.C one-statement theorem, which packages: starts at zero, peaks at $S_{\max}$ at $t_{\mathrm{Page}}$, returns to zero at $2 t_{\mathrm{Page}}$, stays non-negative, and inhabits the master-theorem hypothesis PageCurveDerived.
Together with the peak, end, non-negativity, and post-evaporation lemmas, it closes the kinematic half of Track 3.C (structural theorem, 0 sorry). The dynamical derivation from RS substrate (replica wormholes, quantum extremal surfaces, ledger-side back-reaction) remains explicitly future work. No direct appeal to T0–T8 or the RCL is needed here; the result is pure shape bookkeeping for the gravity track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.