Gravity Page Curve Operator Entropy Schmidt Saturated Process Inhabited

The existence proof

The declaration schmidtSaturatedProcess_inhabited is a machine-checked proof that at least one example of a certain kind of physical process exists. The process in question is a simplified model of a black hole evaporating by emitting radiation. The proof shows there is a version of this model where the entropy, a measure of how much information is hidden, is not an extra assumption but is calculated from the quantum state at every step.

This model works with a tiny toy universe containing only one unit of each type of system, the black hole and the radiation. It runs for a single tick, a single step of time. In this minimal setup, the calculation of entropy from the state always gives zero, because there is nowhere for information to hide. The proof is a simple check of the two possible cases: before the tick and after it.

The importance of this existence proof is architectural. It demonstrates that the framework's definition of a process where entropy is derived from the state is not an empty one. It is a consistent idea that can be built. This is the first step in a larger argument that the famous triangular Page curve, which describes how a black hole's entropy changes as it evaporates, can be derived from more basic principles rather than being put in by hand.

In Recognition Science, this is part of a chain of reasoning about how information is preserved. The proof does not show that real black holes behave this way. It does not claim that the toy model is physically realistic. It only establishes that the formal definition of a state-derived entropy process is coherent and has at least one instance, which is a necessary foundation for the later, more substantive theorems about the Page curve.

What this proof does not do is assert anything about the real world. It is a statement about the consistency of a mathematical model. The model's entropy is zero throughout, which is a special case, not a general result. The proof does not show that a more complex model with non-zero entropy can be built, nor does it show that the Page curve is a physical law. It is a purely logical guarantee that a certain definition is not self-contradictory.

The practical consequence is that the framework can now build on this foundation. Since the existence of a state-derived entropy process is proven, the next step, which is to show that such a process always produces the Page curve, is a meaningful and well-founded question. The existence proof is the load-bearing first stone in that larger construction.

theorem schmidtSaturatedProcess_inhabited :
    Nonempty (SchmidtSaturatedOperatorProcess (Fin 1) (Fin 1)) :=
  ⟨canonicalSchmidtSaturatedProcess⟩

/-- 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 schmidtSaturatedProcess_inhabited :
    Nonempty (SchmidtSaturatedOperatorProcess (Fin 1) (Fin 1)) :=
  ⟨canonicalSchmidtSaturatedProcess⟩

What this page does not claim

This proof does not claim that real black holes evaporate in this way. This proof does not show that any physically realistic process exists. This proof does not establish the Page curve for any system with non-zero entropy.

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: