Gravity Page Curve Structural Triangle Page Curve Phase2 Anti Monotone

The descent phase

The Page curve describes how the entropy of a black hole's radiation changes as the hole evaporates. In its standard triangular form, the curve rises linearly to a peak at the Page time, then falls linearly back to zero at full evaporation. The declaration trianglePageCurve_phase2_anti_monotone is a theorem about that second, descending leg: it states that on the interval from the Page time to twice the Page time, the curve never increases. If t1 and t2 are two times in that window with t1 before t2, the radiation entropy at t2 is less than or equal to the entropy at t1.

This is a purely mathematical statement about a piecewise-linear function, not a physical law. The function itself is defined in the framework's machine-checked library: it takes a peak entropy S_max, a Page time t_Page, and a time t, and returns a number. Before t_Page it climbs at a constant rate; between t_Page and 2·t_Page it descends at a constant rate; after that it is zero. The theorem's content is that the descending leg is monotone decreasing, assuming the peak entropy is nonnegative and the Page time is positive. It is one of several shape properties proved for this function, alongside facts that the curve starts at zero, peaks at S_max, returns to zero at 2·t_Page, and never goes negative.

The theorem matters because it pins down the structural shape that any dynamical derivation of the Page curve must reproduce. The framework's master plan calls for deriving the curve from ledger-based evaporation dynamics, but that derivation is not yet complete. This declaration supplies only the kinematic skeleton: the triangle's rise and fall. It does not claim that real black holes follow this exact curve, nor that the framework has derived the curve from first principles. The descent's monotonicity is a property of a chosen model, not a measurement of nature.

What the theorem does establish is a clean target. Future work in the framework aims to show that the actual radiation entropy, computed from ledger dynamics, matches this triangular shape. Until then, the descent phase is a proved property of a defined function, and the physical claim remains open.

/-- 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

/-- **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

This theorem does not claim that real black hole radiation entropy follows this curve. It does not derive the Page curve from ledger-based dynamics. It does not claim the curve is strictly decreasing, only weakly monotone.

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: