Gravity Page Curve Structural Triangle Page Curve Neg Zero

The zero before the start

The declaration named trianglePageCurve_neg_zero is a theorem in the framework's machine-checked library of formal theorems. It states a simple fact about the triangular Page curve, the standard graph used to describe how the entropy of radiation emitted by an evaporating black hole changes over time. For any negative time, before the evaporation process begins, the radiation entropy is zero. The theorem proves that the function defining this curve returns zero for all negative inputs, a convention that matches the physical picture of a black hole that has not yet started to radiate.

This result is one of several shape properties that the framework has proved about the triangular Page curve. Together they establish the curve's kinematic content: it starts at zero entropy, rises linearly to a peak at the Page time, falls linearly back to zero at twice the Page time, and remains at zero afterward. The Page curve itself describes the competition between the entropy of the emitted radiation and the entropy of the remaining black hole. Early on, the radiation entropy grows as Hawking quanta accumulate. At the Page time, when half the black hole has evaporated, the radiation entropy reaches its maximum, equal to the remaining black hole's thermodynamic entropy. After that, the radiation entropy decreases as the radiation becomes entangled with itself instead of with the hole, until full evaporation restores a pure state with zero radiation entropy.

The theorem about negative time is a boundary condition: it pins down the curve's behavior before the story starts. It is proved directly from the definition of the curve, which sets the value to zero for any time less than or equal to zero. The proof is a routine unfolding of the definition, requiring no additional assumptions about the physics of black hole evaporation. It is part of a larger certified package that also proves the curve is non-negative, peaks correctly, and returns to zero at the end, all with zero unproved axioms in the framework's logical system.

In Recognition Science, this theorem is a step toward a larger goal: deriving the Page curve from the framework's foundational principles. But the theorem itself is only about the shape of the curve, not about where that shape comes from. The framework's library explicitly states that the dynamical derivation, the process of showing that the actual radiation entropy of a real black hole follows this triangular form from first principles, remains future work. The theorem establishes the shape that any such derivation must reproduce, not the derivation itself.

The practical consequence is that the framework now has a certified, machine-checked statement of the curve's behavior before evaporation begins. This is a small but necessary piece of the larger structural result. It means that any future work on the full Page curve derivation can rely on this boundary condition as a proven fact, instead of as an assumption. It also means the framework's library contains a complete, checkable description of the curve's overall shape, from before the start to after the end.

/-- `S_rad(t) = 0` for `t < 0` (convention: no radiation before the
start). -/
theorem trianglePageCurve_neg_zero (S_max t_Page t : ℝ) (h : t < 0) :
    trianglePageCurve S_max t_Page t = 0 := by
  unfold trianglePageCurve
  simp [le_of_lt h]

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

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

/-- `S_rad(t) = 0` for `t > 2·t_Page`: after full evaporation, no
radiation entropy remains. -/
theorem trianglePageCurve_after_end_zero (S_max t_Page t : ℝ)
    (h_t_Page : 0 < t_Page) (h_t : 2 * t_Page < t) :
    trianglePageCurve S_max t_Page t = 0 := by
  unfold trianglePageCurve
  have h_not_zero : ¬ t ≤ 0 := by push_neg; linarith
  have h_not_phase1 : ¬ t ≤ t_Page := by push_neg; linarith
  have h_not_phase2 : ¬ t ≤ 2 * t_Page := by push_neg; linarith
  simp [h_not_zero, h_not_phase1, h_not_phase2]

theorem pageCurveStructuralCert_inhabited :
    Nonempty PageCurveStructuralCert :=
  ⟨pageCurveStructuralCert⟩

What this page does not claim

The theorem does not derive the Page curve from the framework's foundational principles. The theorem does not prove that any real black hole's radiation entropy follows this curve. The theorem does not address the behavior of the curve at exactly zero time, which is covered by a separate theorem.

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: