Gravity Page Curve Dynamical Page Curve From Ledger Ticks At Page Fraction

The derived curve

In the physics of black holes, the Page curve describes how the entropy of a black hole and its emitted radiation changes as the hole evaporates. The curve starts at the black hole's full entropy, falls to a peak at half-evaporation, and returns to zero when the hole is gone. For decades this shape was an expectation, not a derivation; it was drawn from physical intuition rather than proved from a deeper rule.

The standard derivation in quantum information uses Schmidt's theorem, which says that for a pure joint state of two systems, the entropy of one system equals the entropy of the other. If the black hole and its radiation together form a pure state, their entropies must match at every moment. The entropy of each side is also limited by the size of its Hilbert space, the mathematical arena of its possible states. The radiation entropy therefore equals the smaller of two capacity bounds: the bulk capacity, which shrinks linearly as the hole evaporates, and the radiation capacity, which grows linearly as quanta escape. Taking the minimum of these two monotone bounds produces exactly the triangular Page curve, with the peak forced at the halfway point.

In Recognition Science, the framework models this evaporation as a discrete process of recognition ticks, where each tick transfers a fraction of capacity from the bulk ledger to the radiation ledger. The declaration pageCurveFromLedgerTicks defines the curve at a discrete tick count: it is the minimum of the bulk capacity remaining after n ticks and the radiation capacity accumulated after n ticks. The framework's machine-checked library of formal theorems proves the key properties: the radiation entropy is zero at the start, returns to zero at full evaporation, and reaches half the initial black hole entropy at the page time of half-evaporation. The theorem S_rad_at_page_time establishes that the peak value is exactly S_BH / 2, and the theorem information_preservation shows the curve returns to zero, meaning no information is lost in this model.

What the declaration does not claim is that the capacity evolution itself is derived from the recognition update. The linear transfer of capacity is an assumption, a modeling choice for the canonical case. The framework's own notes state that choosing different capacity evolutions would give different curves, for instance for non-uniform Hawking emission rates. Deriving the capacity transfer rate from the recognition ticks themselves remains open, targeted for future work. The declaration also does not claim that this discrete-tick curve is the same as the continuous-time Page curve; it is a discrete approximation defined at tick fractions, and the equality with the continuous form is a separate statement about the limit.

theorem S_rad_at_zero : P.S_rad 0 = 0 := by
  rw [P.schmidt_purification, pageCurveFromUnitarity_at_zero _ P.S_BH_nonneg]

theorem S_rad_at_one : P.S_rad 1 = 0 := by
  rw [P.schmidt_purification, pageCurveFromUnitarity_at_one _ P.S_BH_nonneg]

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

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

/-- The ledger-tick Page curve: the smaller of remaining-bulk capacity and
emitted-radiation capacity. -/
noncomputable def pageCurveFromLedgerTicks (S_BH : ℝ) (N n : ℕ) : ℝ :=
  min (bulkCapacityFromTicks S_BH N n) (radiationCapacityFromTicks S_BH N n)

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

What this page does not claim

The capacity evolution is derived from the recognition update. The discrete-tick curve is identical to the continuous-time Page curve. The peak at half-evaporation is a consequence of the recognition ticks themselves.

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: