trianglePageCurve_phase2_anti_monotone
plain-language theorem explainer
On the descent window from Page time to twice Page time, the triangular Page curve is weakly monotone decreasing. Gravity and QI researchers assembling the kinematic Page-curve shape cite this for the late-time unimodality leg. The proof unfolds the piecewise definition and case-splits on whether the left endpoint still sits at the peak or both times already lie in linear descent, finishing by non-negative slope arithmetic.
Claim. Let $S_{\max}\ge 0$ and $t_{\mathrm{Page}}>0$. For all real $t_1,t_2$ with $t_{\mathrm{Page}}\le t_1\le t_2\le 2 t_{\mathrm{Page}}$, the triangular Page curve $S$ satisfies $S(t_2)\le S(t_1)$. Here $S$ rises linearly from $0$ to $S_{\max}$ on $[0,t_{\mathrm{Page}}]$ and falls linearly from $S_{\max}$ back to $0$ on $[t_{\mathrm{Page}},2 t_{\mathrm{Page}}]$.
background
This module supplies the kinematic content of Track 3.C of the quantum-gravity master plan: the triangular Page curve as a piecewise-linear radiation-entropy-vs-time shape, without the full replica-wormhole or ledger-evaporation dynamics.
The curve is parameterized by peak entropy $S_{\max}$ and Page time $t_{\mathrm{Page}}$. 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 from $S_{\max}$ back to $0$. Phase 3 ($t>2 t_{\mathrm{Page}}$) is identically zero. Early radiation is treated as approximately thermal; after Page time the remaining black-hole thermodynamic entropy binds the radiation entropy downward until full evaporation restores a pure global state.
Sibling results already record the values at zero, at the peak, and at the end, plus non-negativity and phase-1 ascent monotonicity. The present lemma is the matching phase-2 descent anti-monotonicity.
proof idea
Fix $t_1\le t_2$ inside the closed phase-2 window and unfold the piecewise definition. Both times are strictly positive (since $t_{\mathrm{Page}}>0$), so the non-positive branch is excluded. The slope $S_{\max}/t_{\mathrm{Page}}$ is non-negative.
Case on $t_1\le t_{\mathrm{Page}}$. Antisymmetry with the lower bound forces $t_1=t_{\mathrm{Page}}$. If also $t_2\le t_{\mathrm{Page}}$, then $t_2=t_{\mathrm{Page}}$ and both sides equal $S_{\max}$. If $t_2>t_{\mathrm{Page}}$, the claim reduces to $S_{\max}-\mathrm{slope}\cdot(t_2-t_{\mathrm{Page}})\le S_{\max}$, which follows because the subtracted term is non-negative (field_simp, linarith).
If $t_1>t_{\mathrm{Page}}$, both points lie strictly in phase 2. Values are $S_{\max}-\mathrm{slope}\cdot(t-t_{\mathrm{Page}})$; the map $t\mapsto t-t_{\mathrm{Page}}$ is monotone, multiplication by the non-negative slope preserves the inequality, and linarith finishes.
why it matters
Track 3.C needs a structural witness that a triangular Page curve exists with the classical shape properties: starts at zero, peaks at $S_{\max}$ at Page time, returns to zero at $2 t_{\mathrm{Page}}$, stays non-negative, and is unimodal in the strong piecewise sense. Phase-2 anti-monotonicity is one unimodality leg, paired with the phase-1 ascent lemma.
The module is marked structural theorem (zero sorry), closing the kinematic half of the Page-curve derivation while full ledger-side evaporation, back-reaction, and unitary evolution on bulk-plus-radiation remain estimated at 6-10 sessions in the master plan. Sibling packaging results assemble these shape facts into the master-theorem hypothesis witness for a Page-curve-derived structural proposition.
No forcing-chain landmark (T0-T8) or Recognition Composition Law identity is invoked here; this is gravity-track kinematic content rather than foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.