Gravity Page Curve Operator Entropy Schmidt Saturated Entropy Peak

The entropy peak

The Page curve describes how the entropy of radiation emitted by an evaporating black hole changes over time. It starts at zero, rises to a maximum, and then falls back to zero when evaporation completes. This shape resolves a paradox: if information is preserved, the radiation entropy cannot keep growing forever; it must eventually decrease. The peak occurs at the Page time, when roughly half the black hole has evaporated.

In the Recognition Science framework, an operator process models this evaporation as a sequence of discrete ticks, each applying a unitary operation to a combined system of black hole and radiation. The framework defines a Schmidt capacity bound, the maximum entropy consistent with quantum purification, as the minimum of the bulk and radiation capacities at each tick. A process is Schmidt-saturated when its entropy, derived from the state itself, equals this bound at every tick.

The theorem schmidtSaturated_entropy_peak states that in any such saturated process, at the tick where the evaporation fraction is one half, the derived entropy equals exactly S_BH / 2, where S_BH is the initial black hole entropy. This is a structural result: the entropy is not supplied as an independent function but is computed from the evolving state, and saturation alone forces the peak value. The theorem follows directly from the more general result that saturation implies the full Page curve equality at every tick.

What the theorem does not claim is that any real black hole actually saturates the bound. The framework proves a conditional statement: if a process saturates, then the peak occurs. Whether physical evaporation achieves saturation remains an open question. The theorem also does not establish the value of S_BH itself, which is a separate input to the process.

/-- At the Page fraction, the derived readout peaks at S_BH / 2. -/
theorem schmidtSaturated_entropy_peak
    {β ρ : Type} [Fintype β] [DecidableEq β] [Fintype ρ] [DecidableEq ρ]
    (P : SchmidtSaturatedOperatorProcess β ρ) (n : ℕ)
    (hn : n ≤ P.totalTicks)
    (hhalf : evaporationFractionFromTicks P.totalTicks n = 1 / 2) :
    P.entropyFromState (stateAfterOperatorTicks P.unitaryTick n P.initialState) =
      P.S_BH / 2 := by
  rw [schmidtSaturated_entropy_eq_pageCurve P n hn]
  exact pageCurveFromLedgerTicks_at_page_fraction
    P.S_BH P.totalTicks n P.totalTicks_pos hn hhalf

/-- An operator Page process with Schmidt-saturating entropy.  The entropy
functional tracks the state evolution (via `entropyFromState`), and the
radiation entropy at each tick equals the Schmidt capacity bound.

The key structural content: the entropy is *derived from the state* through
`entropyFromState`, not supplied as an independent function. The saturation
hypothesis `saturates` then forces the readout to equal the Page curve. -/
structure SchmidtSaturatedOperatorProcess
    (β ρ : Type) [Fintype β] [DecidableEq β] [Fintype ρ] [DecidableEq ρ]
    extends OperatorPageProcess β ρ where
  entropyFromState : BulkRadiationLedger β ρ → ℝ
  entropyFromState_initial_zero : entropyFromState initialState = 0
  saturates :
    ∀ n : ℕ, n ≤ totalTicks →
      entropyFromState (stateAfterOperatorTicks unitaryTick n initialState) =
        schmidtCapacityBound toOperatorPageProcess n

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

The theorem does not prove that any real black hole saturates the Schmidt bound. The theorem does not determine the numerical value of S_BH. The theorem does not address whether evaporation in nature follows the discrete tick model.

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: