Encyclopedia Gravity Gravity Page Curve Structural Triangle Page Curve Phase1 Monotone

ARTICLE 4 claims 4 theorems

Gravity Page Curve Structural Triangle Page Curve Phase1 Monotone

A theorem about a triangle-shaped curve pins down the early growth of entropy in a model of black hole evaporation, and says nothing about the physics that produces it.

Verify this page

The rising side of the curve

The Page curve describes how the entropy of radiation emitted by an evaporating black hole changes over time. In the simplest model, the curve is a triangle: it rises steadily to a peak, falls steadily back to zero, and stays at zero afterward. The peak marks the Page time, when half the black hole has evaporated and the radiation entropy is largest.

The declaration trianglePageCurve_phase1_monotone is a theorem about the rising side of that triangle. It states that, under the assumptions that the peak entropy is non-negative and the Page time is positive, the curve never decreases during the first phase: for any two times between the start and the Page time, the later time has entropy at least as large as the earlier time. In plainer terms, the radiation entropy only grows during the early stage of evaporation. This is the monotone property, meaning the curve moves in one direction only, here upward, without any dips or reversals.

The theorem is part of a larger machine-checked library of formal theorems. The library proves this and related shape properties of the triangular curve: it starts at zero, peaks at the Page time, returns to zero at full evaporation, and is never negative. These results are kinematic, describing the geometry of the curve itself. They do not derive the curve from any deeper physical principle, such as the quantum mechanics of black holes or the dynamics of evaporation.

What the theorem does not claim is just as important as what it proves. It does not say that the triangular shape is the actual Page curve of a real black hole. It does not derive the curve from the ledger structure that the Recognition Science framework uses to model quantum gravity. It does not show that radiation entropy really does grow linearly in time. The theorem only certifies the shape: if a curve has this triangular form, then its rising side is monotone. The physical derivation that would produce this shape from first principles remains future work.

THEOREM trianglePageCurve_phase1_monotone · IndisputableMonolith/Gravity/PageCurveStructural.lean
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
THEOREM trianglePageCurve_phase1_monotone · IndisputableMonolith/Gravity/PageCurveStructural.lean
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
THEOREM trianglePageCurve_at_zero · trianglePageCurve_at_peak · trianglePageCurve_at_end · trianglePageCurve_nonneg · 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]
THEOREM page_curve_one_statement · IndisputableMonolith/Gravity/PageCurveStructural.lean
page_curve_one_statement · IndisputableMonolith/Gravity/PageCurveStructural.lean:318 
/-- **TRACK 3.C ONE-STATEMENT** (structural form). The triangular Page
curve is theorem-grade in its kinematic content: starts at zero,
peaks at `S_max` at the Page time `t_Page`, returns to zero at full
evaporation `2·t_Page`, is non-negative throughout, and vanishes
after full evaporation. The master theorem hypothesis input
`PageCurveDerived` is inhabited by `pageCurveDerivedWitness`. The
**dynamical derivation** from RS substrate first principles (replica
wormholes, QES, ledger-side back-reaction) remains future multi-session
work. -/
theorem page_curve_one_statement :
    (∀ S t, trianglePageCurve S t 0 = 0) ∧
    (∀ S t, 0 < t → trianglePageCurve S t t = S) ∧
    (∀ S t, 0 < t → trianglePageCurve S t (2 * t) = 0) ∧
    (∀ S t r, 0 ≤ S → 0 < t → 0 ≤ trianglePageCurve S t r) ∧
    (Nonempty Gravity.MasterTheorem.PageCurveDerived) :=
  ⟨trianglePageCurve_at_zero,
   trianglePageCurve_at_peak,
   trianglePageCurve_at_end,
   trianglePageCurve_nonneg,
   ⟨pageCurveDerivedWitness⟩⟩

What this page does not claim

The theorem does not derive the triangular Page curve from the ledger structure or any other first principle. The theorem does not show that the radiation entropy of a real black hole follows this triangular shape. The theorem does not prove that the linear ascent is physically realized; it only certifies the monotone property of a defined 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