Gravity Page Curve Operator Entropy Operator Derived Page Curve Prop Holds

The derived Page curve

The Page curve describes how the entropy of a black hole's radiation changes as the hole evaporates. It starts at zero, rises to a peak when about half the hole has evaporated, and then falls back to zero. This triangular shape is famous because it resolves the black hole information paradox: information is not lost, it is encoded in the radiation. In quantum mechanics, this entropy is the von Neumann entropy of the radiation subsystem, and the peak value is half the initial entropy of the black hole.

A machine-checked library of formal theorems now derives this curve from a more basic process. The framework models the evaporation as a sequence of discrete steps, or ticks (a single step in a discrete process), on a joint state of the black hole and its radiation. At each tick, the radiation's entropy is bounded by a quantity called the Schmidt capacity, which is the maximum entropy allowed by quantum purification of a pure joint state. The key theorem states that if the radiation's entropy, which is derived from the quantum state itself, saturates this bound at every tick, then the entropy must equal the Page curve. This is a structural result: the curve is not an assumption but a consequence of saturation.

The proof establishes the existence of a process that meets these conditions. It constructs a canonical example with a single tick, where the entropy is identically zero, and proves the saturation property holds. The declaration operatorDerivedPageCurveProp_holds is the formal statement that such a process exists. This witness routes through the derived theorem, not through any supplied field, meaning the Page curve is genuinely derived from the operator process rather than being put in by hand. The same library also proves that the derived entropy starts at zero, returns to zero at full evaporation, and peaks at half the initial entropy at the Page fraction.

In Recognition Science, this is a step toward showing that gravity's information structure follows from its foundational principles. The result is a structural theorem, checked with no unproven assumptions. What it does not claim is that this toy model describes a real, four-dimensional black hole. The process is defined on a finite, two-dimensional system with a single tick. The physical bridge from this abstract operator process to actual gravitational evaporation remains an open target, not a proved result.

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

theorem operatorDerivedPageCurveProp_holds : operatorDerivedPageCurveProp :=
  ⟨canonicalSchmidtSaturatedProcess, trivial⟩

/-- The derived readout starts at zero. -/
theorem schmidtSaturated_entropy_zero
    {β ρ : Type} [Fintype β] [DecidableEq β] [Fintype ρ] [DecidableEq ρ]
    (P : SchmidtSaturatedOperatorProcess β ρ) :
    P.entropyFromState (stateAfterOperatorTicks P.unitaryTick 0 P.initialState) = 0 := by
  rw [schmidtSaturated_entropy_eq_pageCurve P 0 (Nat.zero_le P.totalTicks)]
  exact pageCurveFromLedgerTicks_at_zero P.S_BH P.totalTicks P.S_BH_nonneg P.totalTicks_pos

/-- The derived readout returns to zero at full evaporation. -/
theorem schmidtSaturated_entropy_full
    {β ρ : Type} [Fintype β] [DecidableEq β] [Fintype ρ] [DecidableEq ρ]
    (P : SchmidtSaturatedOperatorProcess β ρ) :
    P.entropyFromState
      (stateAfterOperatorTicks P.unitaryTick P.totalTicks P.initialState) = 0 := by
  rw [schmidtSaturated_entropy_eq_pageCurve P P.totalTicks le_rfl]
  exact pageCurveFromLedgerTicks_at_full P.S_BH P.totalTicks P.S_BH_nonneg P.totalTicks_pos

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

What this page does not claim

This result does not describe a real, four-dimensional black hole; the example is a finite toy model with a single tick. The theorem does not prove that any actual evaporating black hole saturates the Schmidt capacity bound. The physical bridge from this abstract operator process to gravitational evaporation is not established here.

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: