Encyclopedia Gravity Gravity Page Curve Structural

ARTICLE 3 claims 2 theorems 1 open

Gravity Page Curve Structural

A triangular curve that maps how a black hole's radiation entropy rises, peaks, and falls to zero, now locked in as a formal theorem.

Verify this page

The structural Page curve

The Page curve is the standard plot in black hole physics of how the entropy of Hawking radiation changes as a black hole evaporates. In the 1970s, Stephen Hawking's calculation suggested information would be lost forever, a paradox. In 1993, Don Page argued the curve must instead rise, peak at the halfway point, and then fall back to zero, meaning all information eventually returns. The structural Page curve takes that triangular shape and proves its basic properties as formal theorems in a machine-checked library.

The curve is defined by a simple piecewise-linear function, S_rad(t), which describes the radiation's entropy at time t. It starts at zero, rises linearly to a maximum value S_max at the Page time t_Page, then falls linearly back to zero at time 2·t_Page, and remains zero afterward. The structural results establish the essential facts: the curve starts at zero, peaks at S_max, returns to zero at full evaporation, is never negative, and is monotone increasing before the peak and monotone decreasing after it. These are not assumptions but theorem-grade results, checked with zero gaps in the proof.

In Recognition Science, the framework models reality as a discrete record of events, and this structural result is Track 3.C of its quantum-gravity master plan. It provides a formal witness that the structural shape of the Page curve exists, satisfying a hypothesis in the framework's conditional master theorem. This is the kinematic content: the shape that any dynamical derivation must reproduce. The full dynamical derivation, from first principles of the ledger to the actual evaporation dynamics, remains future work, estimated at six to ten sessions.

What the structural result does not do is derive the curve from underlying physics. It takes the triangular shape as given and proves its properties. The physical mechanism that produces this shape, the replica wormholes and quantum extremal surfaces, is out of scope. The value of this result is that it retires the placeholder of zero entropy and establishes a concrete, provable target for future work. A reader can now see exactly what a complete derivation must produce: a curve that rises, peaks, and falls, preserving information.

THEOREM trianglePageCurve_at_zero · trianglePageCurve_at_peak · trianglePageCurve_at_end · trianglePageCurve_nonneg · trianglePageCurve_phase1_monotone · trianglePageCurve_phase2_anti_monotone · IndisputableMonolith/Gravity/PageCurveStructural.lean
trianglePageCurve_at_zero · IndisputableMonolith/Gravity/PageCurveStructural.lean:112 
/-- `S_rad(0) = 0`: at the start, no radiation has been emitted. -/
theorem trianglePageCurve_at_zero (S_max t_Page : ℝ) :
    trianglePageCurve S_max t_Page 0 = 0 := by
  unfold trianglePageCurve
  simp
trianglePageCurve_at_peak · IndisputableMonolith/Gravity/PageCurveStructural.lean:118 
/-- `S_rad(t_Page) = S_max`: at the Page time, the radiation entropy
reaches its peak. -/
theorem trianglePageCurve_at_peak (S_max t_Page : ℝ) (h : 0 < t_Page) :
    trianglePageCurve S_max t_Page t_Page = S_max := by
  unfold trianglePageCurve
  have h_pos : ¬ t_Page ≤ 0 := not_le.mpr h
  have h_t_ne : t_Page ≠ 0 := ne_of_gt h
  simp [h_pos]
  field_simp
trianglePageCurve_at_end · IndisputableMonolith/Gravity/PageCurveStructural.lean:128 
/-- `S_rad(2·t_Page) = 0`: at full evaporation, the radiation entropy
returns to zero (information preservation). -/
theorem trianglePageCurve_at_end (S_max t_Page : ℝ) (h : 0 < t_Page) :
    trianglePageCurve S_max t_Page (2 * t_Page) = 0 := by
  unfold trianglePageCurve
  have h2_pos : ¬ (2 * t_Page) ≤ 0 := by
    push_neg; linarith
  have h_not_phase1 : ¬ (2 * t_Page) ≤ t_Page := by
    push_neg; linarith
  have h_t_ne : t_Page ≠ 0 := ne_of_gt h
  simp [h2_pos, h_not_phase1]
  field_simp
  ring
trianglePageCurve_nonneg · IndisputableMonolith/Gravity/PageCurveStructural.lean:162 
/-- The Page curve is non-negative everywhere, assuming `0 ≤ S_max`
and `0 < t_Page`. -/
theorem trianglePageCurve_nonneg
    (S_max t_Page t : ℝ) (h_S : 0 ≤ S_max) (h_t_Page : 0 < t_Page) :
    0 ≤ trianglePageCurve S_max t_Page t := by
  unfold trianglePageCurve
  by_cases h0 : t ≤ 0
  · simp [h0]
  · simp [h0]
    by_cases h1 : t ≤ t_Page
    · simp [h1]
      have : 0 ≤ t := by push_neg at h0; linarith
      have h_slope : 0 ≤ S_max / t_Page := div_nonneg h_S (le_of_lt h_t_Page)
      exact mul_nonneg h_slope this
    · simp [h1]
      by_cases h2 : t ≤ 2 * t_Page
      · simp [h2]
        have h_decline : S_max / t_Page * (t - t_Page) ≤ S_max := by
          have h_tail : t - t_Page ≤ t_Page := by linarith
          have h_slope : 0 ≤ S_max / t_Page :=
            div_nonneg h_S (le_of_lt h_t_Page)
          have h_t_pos : 0 ≤ t - t_Page := by
            push_neg at h1; linarith
          calc S_max / t_Page * (t - t_Page)
              ≤ S_max / t_Page * t_Page :=
                mul_le_mul_of_nonneg_left h_tail h_slope
            _ = S_max := by field_simp
        linarith
      · simp [h2]
trianglePageCurve_phase1_monotone · IndisputableMonolith/Gravity/PageCurveStructural.lean:192 
/-- Phase-1 (ascent) monotonicity: on `[0, t_Page]`, the Page curve is
weakly monotone increasing. -/
theorem trianglePageCurve_phase1_monotone
    (S_max t_Page : ℝ) (h_S : 0 ≤ S_max) (h_t_Page : 0 < t_Page) :
    ∀ t1 t2, 0 ≤ t1 → t1 ≤ t2 → t2 ≤ t_Page →
      trianglePageCurve S_max t_Page t1 ≤ trianglePageCurve S_max t_Page t2 := by
  intro t1 t2 h_t1 h_t12 h_t2
  have h_t2_pos : 0 ≤ t2 := le_trans h_t1 h_t12
  unfold trianglePageCurve
  have h_t1_not_neg : ¬ t1 < 0 := not_lt.mpr h_t1
  have h_t2_not_neg : ¬ t2 < 0 := not_lt.mpr h_t2_pos
  by_cases h_t1_zero : t1 ≤ 0
  · -- t1 ≤ 0: LHS = 0
    have h_t1_eq : t1 = 0 := le_antisymm h_t1_zero h_t1
    by_cases h_t2_zero : t2 ≤ 0
    · have h_t2_eq : t2 = 0 := le_antisymm h_t2_zero h_t2_pos
      simp [h_t1_zero, h_t2_zero]
    · simp [h_t1_zero, h_t2_zero, h_t2]
      have h_slope : 0 ≤ S_max / t_Page := div_nonneg h_S (le_of_lt h_t_Page)
      exact mul_nonneg h_slope h_t2_pos
  · push_neg at h_t1_zero
    have h_t2_pos' : 0 < t2 := lt_of_lt_of_le h_t1_zero h_t12
    have h_t1_not_zero : ¬ t1 ≤ 0 := not_le.mpr h_t1_zero
    have h_t2_not_zero : ¬ t2 ≤ 0 := not_le.mpr h_t2_pos'
    simp [h_t1_not_zero, h_t2_not_zero, le_trans h_t12 h_t2, h_t2]
    have h_slope_nn : 0 ≤ S_max / t_Page := div_nonneg h_S (le_of_lt h_t_Page)
    exact mul_le_mul_of_nonneg_left h_t12 h_slope_nn
trianglePageCurve_phase2_anti_monotone · IndisputableMonolith/Gravity/PageCurveStructural.lean:220 
/-- Phase-2 (descent) anti-monotonicity: on `[t_Page, 2·t_Page]`, the
Page curve is weakly monotone decreasing. -/
theorem trianglePageCurve_phase2_anti_monotone
    (S_max t_Page : ℝ) (h_S : 0 ≤ S_max) (h_t_Page : 0 < t_Page) :
    ∀ t1 t2, t_Page ≤ t1 → t1 ≤ t2 → t2 ≤ 2 * t_Page →
      trianglePageCurve S_max t_Page t2 ≤ trianglePageCurve S_max t_Page t1 := by
  intro t1 t2 h_t1 h_t12 h_t2
  have h_t1_pos : 0 < t1 := lt_of_lt_of_le h_t_Page h_t1
  have h_t2_pos : 0 < t2 := lt_of_lt_of_le h_t1_pos h_t12
  unfold trianglePageCurve
  have h_t1_not_zero : ¬ t1 ≤ 0 := not_le.mpr h_t1_pos
  have h_t2_not_zero : ¬ t2 ≤ 0 := not_le.mpr h_t2_pos
  have h_slope_nn : 0 ≤ S_max / t_Page := div_nonneg h_S (le_of_lt h_t_Page)
  by_cases h_t1_phase1 : t1 ≤ t_Page
  · have h_t1_eq : t1 = t_Page := le_antisymm h_t1_phase1 h_t1
    by_cases h_t2_phase1 : t2 ≤ t_Page
    · have h_t2_eq : t2 = t_Page := le_antisymm h_t2_phase1 (h_t1_eq ▸ h_t12)
      simp [h_t1_not_zero, h_t2_not_zero, h_t1_phase1, h_t2_phase1]
      rw [h_t1_eq, h_t2_eq]
    · simp [h_t1_not_zero, h_t2_not_zero, h_t1_phase1, h_t2_phase1, h_t2]
      rw [h_t1_eq]
      -- LHS = S_max / t_Page * t_Page = S_max
      -- RHS = S_max - S_max/t_Page * (t2 - t_Page)
      -- Need: RHS ≤ LHS
      have h_diff_nn : 0 ≤ t2 - t_Page := by
        push_neg at h_t2_phase1; linarith
      have h_sub_nn : 0 ≤ S_max / t_Page * (t2 - t_Page) :=
        mul_nonneg h_slope_nn h_diff_nn
      have : S_max / t_Page * t_Page = S_max := by field_simp
      linarith
  · push_neg at h_t1_phase1
    have h_t1_not_phase1 : ¬ t1 ≤ t_Page := not_le.mpr h_t1_phase1
    have h_t2_not_phase1 : ¬ t2 ≤ t_Page := not_le.mpr (lt_of_lt_of_le h_t1_phase1 h_t12)
    simp [h_t1_not_zero, h_t2_not_zero, h_t1_not_phase1, h_t2_not_phase1,
          le_trans h_t12 h_t2, h_t2]
    -- Both in phase 2: S_max - slope*(t-t_Page); larger t → smaller value
    have h_diff_le : t1 - t_Page ≤ t2 - t_Page := by linarith
    have h_prod_le : S_max / t_Page * (t1 - t_Page) ≤ S_max / t_Page * (t2 - t_Page) :=
      mul_le_mul_of_nonneg_left h_diff_le h_slope_nn
    linarith
THEOREM pageCurveDerivedWitness · IndisputableMonolith/Gravity/PageCurveStructural.lean
pageCurveDerivedWitness · IndisputableMonolith/Gravity/PageCurveStructural.lean:282 
/-- **Inhabitant for the master theorem hypothesis input**
`PageCurveDerived` (from `Gravity.MasterTheorem`, Session 97). This
witness retires the Page-curve hypothesis from the conditional master
theorem `rs_quantum_gravity_master_conditional`. -/
def pageCurveDerivedWitness :
    Gravity.MasterTheorem.PageCurveDerived where
  page_curve_derived := page_curve_derived_structural_prop
  holds := page_curve_derived_structural_prop_holds

What this page does not claim

The structural result does not derive the Page curve from physical first principles. The structural result does not prove that the actual radiation entropy of a real black hole follows this shape. The structural result does not resolve the information paradox by itself; it only establishes a target shape.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/PageCurveStructural.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND