IndisputableMonolith.Gravity.PageCurveStructural
Structural Page curve: a triangular piecewise-linear radiation entropy versus time, rising from 0 to S_max by the Page time, falling back to 0 by twice that time, then identically zero. Gravity master-theorem and dynamical Page-curve modules cite it as the kinematic ansatz for evaporation entropy. The module defines the curve and proves elementary shape facts (endpoints, nonnegativity, phase mono/anti-monotonicity) with no dynamics.
claimThe structural Page curve $S_{\mathrm{tri}}(t; t_{\mathrm{Page}}, S_{\max})$ rises linearly from $0$ to $S_{\max}$ on $[0,t_{\mathrm{Page}}]$, falls linearly from $S_{\max}$ to $0$ on $[t_{\mathrm{Page}}, 2t_{\mathrm{Page}}]$, and is identically $0$ for $t>2t_{\mathrm{Page}}$ and for $t<0$. Here $S_{\max}$ is peak radiation entropy and $t_{\mathrm{Page}}$ is the half-evaporation (Page) time.
background
In evaporating black holes the Page curve is the entanglement entropy of Hawking radiation as a function of time. The standard qualitative picture is a rise until roughly half the mass has evaporated (the Page time), then a fall to zero at complete evaporation, restoring purity of the radiation.
This module lives under the Gravity Master Theorem track. It supplies a purely kinematic triangular ansatz with two free parameters: half-evaporation time $t_{\mathrm{Page}}$ and peak entropy $S_{\max}$. No ledger dynamics or Recognition forcing is used; the shape is stipulated by cases on three phases, with negative times set to zero by convention.
Upstream, the module imports the Master Theorem statement infrastructure. Downstream dynamical work treats this triangle as the baseline kinematic curve to be justified or replaced.
proof idea
Definition module plus elementary lemmas on a piecewise-linear function. The core curve is defined by cases: linear ascent on the first phase, linear descent on the second, zero thereafter and for negative time. Companion results record values at $t=0$, at the peak, at the end of evaporation, and after the end; nonnegativity; monotonicity on phase 1; anti-monotonicity on phase 2. A packaged structural proposition asserts the shape properties, and a witness shows that proposition holds. No analytic estimates or RS-specific identities are required.
why it matters in Recognition Science
Feeds three Gravity parents: the deeper-partial master theorem (Page-curve hypothesis pre-filled), the fully structural master theorem (structural witnesses, zero open hypothesis inputs), and the dynamical Page-curve module. The dynamical module explicitly records that this structural module shipped the triangular curve as a kinematic ansatz, which later work derives from Schmidt-balanced ledger dynamics. Within Tracks 7.A and 3.C it closes the Page-curve slot for master-statement authoring while dynamical upgrade remains staged. It does not invoke the T0–T8 forcing chain, RCL, or phi-ladder mass formulae; it is gravity-side structural scaffolding for the entropy-versus-time shape.
scope and limits
- Does not derive the Page curve from ledger, semiclassical, or quantum dynamics.
- Does not fix t_Page or S_max from RS constants or microphysics.
- Does not prove unitarity or information recovery beyond the kinematic shape.
- Does not treat rotating, charged, or higher-dimensional black hole corrections.
- Does not supersede the dynamical Page-curve derivation module.
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