IndisputableMonolith.Gravity.PageCurveStructural
Structural Page curve: a piecewise-linear triangular ansatz for radiation entropy that rises from 0 to S_max by the Page time, falls back to 0 by twice that time, then stays zero. Gravity-track authors cite it as the kinematic skeleton before dynamical ledger work. The module defines the function and proves elementary shape facts (endpoints, nonnegativity, phase monotonicity).
claimThe structural Page curve $S_{\mathrm{tri}}(t; S_{\max}, t_{\mathrm{Page}})$ equals the linear ascent from $0$ to $S_{\max}$ on $[0,t_{\mathrm{Page}}]$, the linear descent from $S_{\max}$ to $0$ on $[t_{\mathrm{Page}}, 2t_{\mathrm{Page}}]$, and $0$ for all $t>2t_{\mathrm{Page}}$ and all $t<0$. Here $S_{\max}$ is peak radiation entropy and $t_{\mathrm{Page}}$ is the half-evaporation (Page) time.
background
In black-hole evaporation, the Page curve is the expected time series of entanglement entropy of Hawking radiation: it grows while the hole is large, peaks near the half-evaporation (Page) time, then falls back so that the final pure state has vanishing radiation entropy. Recognition Science Gravity Track 7 packages this curve as one structural input to the master gravity theorem.
This module supplies only the kinematic ansatz: a triangular, piecewise-linear function fixed by two parameters, peak entropy $S_{\max}$ and Page time $t_{\mathrm{Page}}$. Negative times are set to zero by convention; after full evaporation ($t>2t_{\mathrm{Page}}$) the curve is identically zero. No ledger dynamics or unitarity argument is claimed here.
Upstream, the module sits under Gravity.MasterTheorem (Track 7.A structural master statement). Downstream dynamical work replaces the ansatz by a curve derived from Schmidt-balanced ledger evolution.
proof idea
Definition-first module. The core object is the piecewise-linear trianglePageCurve with three temporal regimes and a negative-time convention. Companion lemmas are direct case splits on those regimes: values at $0$, at the peak, and at the end; vanishing after the end and for negative $t$; global nonnegativity; monotone ascent on phase 1 and anti-monotone descent on phase 2. A bundled structural proposition and witness package those facts for import into master-theorem assemblies. No deep analysis or dynamics; pure elementary real arithmetic on a defined piecewise function.
why it matters in Recognition Science
Gives Gravity Track 7 a named, sorry-free structural stand-in for the Page curve so master-theorem statements can close without waiting on full evaporation dynamics. It is imported by MasterTheoremStructural (fully structural master theorem with all hypothesis inputs pre-filled by structural witnesses), MasterTheoremDeeperPartial (master theorem with PTA, strong-field, and Page-curve hypotheses pre-filled), and PageCurveDynamical (Track 3.C), which upgrades the triangular ansatz to a curve from Schmidt-balanced ledger dynamics. In the RS forcing picture this is scaffolding for the gravity side of the master statement, not a T0–T8 landmark itself; the dynamical upgrade remains the path from structural to unconditional form.
scope and limits
- Does not derive the Page curve from ledger or semiclassical dynamics.
- Does not prove unitarity, purity of the final state, or information recovery.
- Does not fix $S_{\max}$ or $t_{\mathrm{Page}}$ from RS constants or microphysics.
- Does not address greybody factors, backreaction, or higher-curvature corrections.
- Does not claim the physical entropy is exactly piecewise linear; only a structural ansatz.
used by (3)
depends on (1)
declarations in this module (16)
-
def
trianglePageCurve -
theorem
trianglePageCurve_at_zero -
theorem
trianglePageCurve_at_peak -
theorem
trianglePageCurve_at_end -
theorem
trianglePageCurve_after_end_zero -
theorem
trianglePageCurve_neg_zero -
theorem
trianglePageCurve_nonneg -
theorem
trianglePageCurve_phase1_monotone -
theorem
trianglePageCurve_phase2_anti_monotone -
def
page_curve_derived_structural_prop -
theorem
page_curve_derived_structural_prop_holds -
def
pageCurveDerivedWitness -
structure
PageCurveStructuralCert -
def
pageCurveStructuralCert -
theorem
pageCurveStructuralCert_inhabited -
theorem
page_curve_one_statement