Gravity Page Curve Dynamical

The derived Page curve

The Page curve describes how the entropy of a black hole and its radiation changes as the hole evaporates. In ordinary physics, the curve rises, peaks, and falls back to zero, a shape that encodes the idea that information is not lost. For decades this curve was a postulate, a shape physicists believed must be right. The framework called Recognition Science treats this shape as something that can be derived, not assumed.

In Recognition Science, the derivation starts with a ledger, a discrete record of events. The black hole and its radiation are two ledgers whose total capacity is fixed. As time passes, capacity moves from the bulk ledger, the black hole, to the radiation ledger. The fraction of entropy transferred is called t, running from 0 at the start to 1 at full evaporation. The bulk capacity falls as S_BH times (1-t), and the radiation capacity grows as S_BH times t. The sum of the two capacities is always S_BH, a constant.

The key step is Schmidt purification, a theorem from quantum information. When two systems together are in a pure state, the entropy of each part is equal, and both are bounded by the logarithm of the smaller Hilbert space dimension. In this model, the radiation entropy saturates that bound. The result is a curve defined as the minimum of the two capacities: min(bulkCapacity, radiationCapacity). This minimum is the triangular Page curve. The peak at t equals one half is forced by the mathematics, not chosen. The return to zero at t equals one is information preservation.

In the machine-checked library of formal theorems, this result is a structural theorem with zero unproved assumptions. The definitions bulkCapacity and radiationCapacity are linear functions of t. The theorem capacity_sum_invariant proves their sum is constant. The theorem information_preservation proves the curve returns to zero at the end. The theorem S_rad_at_page_time proves the radiation entropy at the midpoint is exactly half the initial black hole entropy. These are all proved in the library, not assumed.

The dynamical step is the recognition tick, the discrete update of the ledger. The evaporation fraction is defined as n divided by N, where n is the number of ticks and N is the total. The curve from ledger ticks uses the same minimum of capacities, now expressed in terms of tick counts. This connects the continuous curve to a discrete process. The remaining open step is to derive the capacity evolution itself from the recognition update, which requires modeling the transfer rate at each tick. That is future work.

What this changes is the status of the Page curve. It is no longer a kinematic ansatz, a shape written down by hand. It is the unique entropy profile compatible with linear capacity transfer and Schmidt purification. The triangular shape is not the only possible curve; different capacity evolutions would give different shapes. But under the canonical linear transfer, the triangle with peak at half-evaporation is derived, not postulated.

/-- The Page curve as the entropy bound forced by Schmidt purification:
`S_rad(t) = min(bulkCapacity, radiationCapacity)`. This is the unique
saturation of the entropy bound on a pure joint state, given linear
capacity transfer between bulk and radiation. -/
def pageCurveFromUnitarity (S_BH t : ℝ) : ℝ :=
  min (bulkCapacity S_BH t) (radiationCapacity S_BH t)

/-- Bulk Hilbert-space entropy capacity at evaporation fraction `t`.
Linear decrease from `S_BH` at `t = 0` to `0` at `t = 1`. -/
def bulkCapacity (S_BH t : ℝ) : ℝ := S_BH * (1 - t)

/-- Radiation Hilbert-space entropy capacity at evaporation fraction `t`.
Linear increase from `0` at `t = 0` to `S_BH` at `t = 1`. -/
def radiationCapacity (S_BH t : ℝ) : ℝ := S_BH * t

@[simp]

/-- Capacity-sum invariant: bulk + radiation = S_BH at every `t`.
Reflects conservation of Hilbert-space capacity under linear transfer. -/
theorem capacity_sum_invariant (S_BH t : ℝ) :
    bulkCapacity S_BH t + radiationCapacity S_BH t = S_BH := by
  unfold bulkCapacity radiationCapacity
  ring

/-- **Information preservation:** the Page curve returns to zero at full
evaporation because the bulk capacity vanishes. This is the unitarity
signature: all entropy initially in the bulk has been transferred to
radiation, and the radiation entropy returns to the pure-state value
(zero) because no remaining bulk degrees of freedom remain to entangle
with. -/
theorem information_preservation (S_BH : ℝ) (hS : 0 ≤ S_BH) :
    pageCurveFromUnitarity S_BH 1 = 0 :=
  pageCurveFromUnitarity_at_one S_BH hS

/-- **The Page time = half-evaporation.** The peak radiation entropy is
reached at `t = 1/2` with value `S_BH / 2`, forced by symmetry of the
capacity transfer. -/
theorem S_rad_at_page_time : P.S_rad (1/2) = P.S_BH / 2 := by
  rw [P.schmidt_purification, pageCurveFromUnitarity_at_half]

What this page does not claim

The capacity evolution is not derived from the recognition update; it is assumed linear in t. This does not prove that information is physically preserved in real black holes; it proves the curve shape under the model's assumptions. The module does not derive the Hawking radiation spectrum or emission rate.

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/PageCurveDynamical.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: