Pith. sign in
module module moderate

IndisputableMonolith.Gravity.PageCurveOperatorEntropy

show as:
view Lean formalization →

Defines the Schmidt capacity bound and a saturated operator Page process whose von Neumann entropy tracks the triangular Page curve exactly. Gravity auditors cite it for the operator-level witness that radiation entropy rises then falls under pure-state Schmidt purification. The module builds the bound from tick-induced evaporation fractions, saturates it, and packages an inhabited process plus a derived Page-curve proposition for master-theorem closure.

claimAt evaporation fraction $f_n$ induced by tick $n$, the Schmidt capacity is $\min(C_{\mathrm{bulk}}, C_{\mathrm{rad}}(f_n))$, the maximum entropy of a pure joint state under Schmidt purification. A Schmidt-saturated operator process is one whose entropy equals this bound at every tick, hence equals the triangular Page curve (zero at the ends, peak at the Page time).

background

Track 3.C derives the black-hole Page curve from Schmidt-balanced ledger dynamics rather than from a kinematic ansatz. The upstream module PageCurveDynamical replaces the Session-101 piecewise-linear template with a structural theorem: entropy is forced by purification of a pure bulk-plus-radiation state on the eight-tick ledger.

This module introduces the capacity that implements that force. The Schmidt capacity bound at tick $n$ is $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$ evaluated at the tick-induced evaporation fraction; it is the largest entropy compatible with a pure joint state. A Schmidt-saturated operator process is an operator Page process whose entropy meets that bound at every tick.

Sibling constructions include the zero, full, and Page-fraction evaluations of the bound, equality of saturated entropy with the Page curve, peak entropy, a canonical inhabited saturated process, and the proposition operatorDerivedPageCurveProp used as a master-theorem witness.

proof idea

Definition-and-lemma layer on top of the dynamical Page-curve module. Capacity bounds are defined pointwise as minima of bulk and radiation capacities at the tick fraction; elementary lemmas record the zero, full-evaporation, and mid-Page values. Saturation is a structure asserting entropy equals the bound at every tick. Equality, endpoint, and peak lemmas then identify that entropy with the triangular Page curve. A canonical saturated process is exhibited and shown inhabited, and the package is reified as the proposition consumed by downstream witnesses. No sorry; proofs are direct unfoldings and arithmetic on the min-bound.

why it matters in Recognition Science

Supplies the operator-level Page-curve witness that closes Gravity Track 3.C for the unconditional master theorem. MasterTheoremUnconditional imports this module to install theorem-built witnesses in place of the older conditional arguments to rs_quantum_gravity_master_conditional. PageCurveNontrivial consumes the shipped operatorPageCurveDerivedWitness and the derived proposition to answer referee F3 (nontrivial Page process).

In the broader RS gravity stack this is the bridge from Schmidt ledger dynamics to a concrete entropy curve: pure-state purification forces the rise-and-fall shape without an external ansatz. It sits downstream of the dynamical structural theorem and upstream of master-theorem and nontriviality closures, so auditors checking zero-axiom Page-curve claims land here.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (18)