Gravity Page Curve Operator Entropy Schmidt Capacity Bound At Page Fraction

The peak of the entropy curve

The Schmidt capacity bound is a ceiling on how much entropy can appear in radiation emitted by an evaporating black hole, set by the requirement that the joint state of the hole and its radiation remains pure. In the framework's discrete model, evaporation proceeds in ticks, and at each tick the bound is the smaller of two capacities: the bulk capacity of the remaining hole and the radiation capacity already emitted. The declaration schmidtCapacityBound_at_page_fraction proves that when the evaporation fraction reaches one half, this bound equals exactly half the initial entropy of the hole, written S_BH / 2. This is the peak of the triangular Page curve, the point where the radiation entropy stops rising and begins to fall.

The theorem is a formal statement in the machine-checked library of formal theorems. It takes an operator Page process, a structure that models evaporation as a sequence of unitary ticks, and a tick number n that does not exceed the total tick count. The condition that the evaporation fraction equals 1/2 is the hypothesis; the conclusion is the equality of the Schmidt capacity bound with S_BH / 2. The proof unfolds the definition of the bound and applies a prior lemma about the Page curve at the page fraction. This is not a numerical simulation or a heuristic; it is a derived equality that follows from the definitions of the model.

The theorem also carries two boundary cases that give the curve its shape. At tick zero, before any evaporation, the bound is zero, because no radiation has been emitted. At the final tick, when the hole has fully evaporated, the bound returns to zero, because information preservation forces the radiation entropy back to zero. These three facts, zero at the start, zero at the end, and half the initial entropy at the midpoint, are the defining features of the triangular Page curve. The framework's theorem establishes them for its operator process model, not for any particular physical black hole.

In Recognition Science, the theorem is part of a larger claim that the Page curve emerges from the operator process rather than being supplied as an input. The structure SchmidtSaturatedOperatorProcess adds a state-derived entropy function and a saturation hypothesis: the radiation entropy at every tick equals the capacity bound. Under that hypothesis, the framework proves the derived readout equals the Page curve at every tick, with no separate field asserting the equality. The peak theorem is the special case at the midpoint, and it holds because the saturation hypothesis forces the readout to track the bound exactly.

What the theorem does not claim is important. It does not assert that any real black hole saturates the Schmidt bound, nor that the framework's discrete tick model is the correct description of actual evaporation. The saturation hypothesis is a structural assumption, not a physical law. The theorem is conditional: if a process saturates, then its entropy peaks at half the initial value at the midpoint. The existence of a canonical saturating process is proved, but it is a toy example with a single tick and zero entropy, not a model of a physical black hole.

/-- The Schmidt bound at the Page fraction equals half the initial entropy. -/
theorem schmidtCapacityBound_at_page_fraction
    {β ρ : Type} [Fintype β] [DecidableEq β] [Fintype ρ] [DecidableEq ρ]
    (P : OperatorPageProcess β ρ) (n : ℕ) (hn : n ≤ P.totalTicks)
    (hhalf : evaporationFractionFromTicks P.totalTicks n = 1 / 2) :
    schmidtCapacityBound P n = P.S_BH / 2 := by
  unfold schmidtCapacityBound
  exact pageCurveFromLedgerTicks_at_page_fraction
    P.S_BH P.totalTicks n P.totalTicks_pos hn hhalf

/-- The Schmidt capacity bound at tick 0 is zero: no radiation entropy before
any evaporation. -/
theorem schmidtCapacityBound_zero
    {β ρ : Type} [Fintype β] [DecidableEq β] [Fintype ρ] [DecidableEq ρ]
    (P : OperatorPageProcess β ρ) :
    schmidtCapacityBound P 0 = 0 := by
  unfold schmidtCapacityBound
  exact pageCurveFromLedgerTicks_at_zero P.S_BH P.totalTicks P.S_BH_nonneg P.totalTicks_pos

/-- The Schmidt capacity bound at full evaporation is zero: information
preservation forces the radiation entropy back to zero. -/
theorem schmidtCapacityBound_full
    {β ρ : Type} [Fintype β] [DecidableEq β] [Fintype ρ] [DecidableEq ρ]
    (P : OperatorPageProcess β ρ) :
    schmidtCapacityBound P P.totalTicks = 0 := by
  unfold schmidtCapacityBound
  exact pageCurveFromLedgerTicks_at_full P.S_BH P.totalTicks P.S_BH_nonneg P.totalTicks_pos

/-- The radiation entropy at tick `n` of a Schmidt-saturated process equals the
Page curve.  This is the derived readout theorem: no `readout_eq_page_curve`
field is needed. -/
theorem schmidtSaturated_entropy_eq_pageCurve
    {β ρ : Type} [Fintype β] [DecidableEq β] [Fintype ρ] [DecidableEq ρ]
    (P : SchmidtSaturatedOperatorProcess β ρ) (n : ℕ) (hn : n ≤ P.totalTicks) :
    P.entropyFromState (stateAfterOperatorTicks P.unitaryTick n P.initialState) =
      pageCurveFromLedgerTicks P.S_BH P.totalTicks n :=
  P.saturates n hn

What this page does not claim

It does not claim that any real black hole saturates the Schmidt bound, only that if one does, its entropy peaks at half the initial value. It does not claim that the framework's discrete tick model is the correct physical description of black hole evaporation. It does not claim that the canonical saturating process is a model of a physical black hole, since it has zero entropy throughout.

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