Gravity Page Curve Structural Triangle Page Curve At Peak

The peak of the curve

The Page curve describes how the entropy of radiation emitted by an evaporating black hole changes over time. In the standard picture, the curve rises as the black hole radiates, reaches a maximum at the Page time, and then falls back to zero when the black hole has fully evaporated. This triangular shape is a central expectation of modern quantum gravity, because it encodes the idea that information is not lost.

The declaration trianglePageCurve_at_peak is a proved theorem in the framework's machine-checked library of formal theorems. It states that at the Page time, the radiation entropy equals its maximum value. In symbols, if S_max is the peak entropy and t_Page is the Page time, then S_rad(t_Page) = S_max. The proof is a direct calculation from the definition of the triangular curve, requiring only that the Page time is positive. This is a statement about the shape of the curve, not about the physics that produces it.

In Recognition Science, this theorem is part of a larger structural result. The framework defines a piecewise-linear function that rises from zero, peaks at S_max, and descends back to zero at twice the Page time. The theorem at the peak is one of several that pin down this shape: the curve starts at zero, peaks at the Page time, returns to zero at full evaporation, and is never negative. Together, these properties form a certificate that the triangular Page curve has the expected kinematic form.

What the theorem does not claim is just as important. It does not derive the Page curve from the fundamental principles of the framework. The dynamical derivation, which would show that actual radiation entropy follows this shape from ledger dynamics, back-reaction, or replica wormholes, remains future work. The theorem establishes the shape that any such derivation must reproduce, not the derivation itself. It also does not assign numerical values to S_max or t_Page; those remain parameters of the curve.

For a reader, the practical consequence is clear. The triangular Page curve is not a placeholder in the framework's library; it is a theorem-grade shape with its key properties proved. But it is a kinematic skeleton, not a dynamical result. The framework has pinned down what the curve must look like, and left the question of why it looks that way open.

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

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

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

/-- **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 Page curve from the framework's fundamental principles. The theorem does not assign numerical values to S_max or t_Page. The theorem does not prove that the actual radiation entropy follows this shape, only that the shape has these properties.

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: