Gravity Page Curve Operator Entropy Operator Page Curve One Statement

The operator-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 at the halfway point, and falls back to zero when evaporation completes. The curve resolves the black hole information paradox by showing that information can escape in the radiation. A machine-checked library of formal theorems, called the framework's library, now proves that this curve follows from a single structural principle.

In Recognition Science, the framework models the evaporation as a discrete process with a ledger of ticks, a record of each step. The central theorem, operator_page_curve_one_statement, establishes three facts together. First, a process exists in which the entropy is derived from the quantum state itself, not supplied as an external function. Second, this derived entropy has all the Page curve properties: it starts at zero, returns to zero at full evaporation, and peaks at half the initial black hole entropy. Third, the proof routes through this operator derivation, not through any assumed equality field.

The key mathematical content is the Schmidt capacity bound, the maximum entropy consistent with the purification of a pure joint state. The theorem proves that when the state-derived entropy saturates this bound, the readout must equal the Page curve at every tick. This is a structural theorem with no unproved assumptions and no framework-specific axioms.

What the declaration does not claim is equally important. It does not claim that any particular physical black hole in nature follows this curve. It establishes a conditional statement: if a process saturates the Schmidt bound, then its entropy readout follows the Page curve. The existence proof uses a minimal one-tick process, which is a mathematical witness, not a physical model. The theorem also does not claim that the Page curve is unique; other curves could arise from non-saturating processes.

The consequence is that the triangular Page curve is not an input but an output of the framework's structure. A reader can now see that the information paradox resolution is a theorem about state-derived entropy, not a postulate about radiation.

/-- **OPERATOR-DERIVED PAGE CURVE ONE-STATEMENT.**  The Schmidt-saturated
operator process exists, the derived readout has all Page-curve properties
(starts at zero, returns to zero, peaks at Page fraction), and the
master-theorem witness routes through the operator derivation without using
`readout_eq_page_curve` as a supplied field. -/
theorem operator_page_curve_one_statement :
    Nonempty (SchmidtSaturatedOperatorProcess (Fin 1) (Fin 1)) ∧
    operatorDerivedPageCurveProp ∧
    Nonempty Gravity.MasterTheorem.PageCurveDerived :=
  ⟨schmidtSaturatedProcess_inhabited,
   operatorDerivedPageCurveProp_holds,
   ⟨operatorPageCurveDerivedWitness⟩⟩

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

/-- 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 claim that any particular physical black hole in nature follows the Page curve. The existence proof uses a minimal one-tick process, which is a mathematical witness, not a physical model. The theorem does not claim that the Page curve is unique; other curves could arise from non-saturating processes.

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: