OperatorPageEntropyReadout
plain-language theorem explainer
Extends the operator-level Page process by a radiation-entropy readout forced to equal the ledger-tick Page curve at every tick up to the evaporation budget. Track 3.C interface and handoff consumers cite this bundle when they need an explicit entropy surface on bulk⊗radiation. Pure structure definition: inherited process fields plus the readout map and its equality constraint; no proof body.
Claim. An operator Page entropy readout on finite bulk and radiation types is an operator-level Page process (black-hole entropy $S_{\mathrm{BH}}\ge 0$, positive tick budget $N$, unitary tick, initial bulk-radiation state) together with a map $S_{\mathrm{rad}}:\mathbb{N}\to\mathbb{R}$ such that for all $n\le N$, $S_{\mathrm{rad}}(n)$ equals the ledger-tick Page curve $\min(\mathrm{bulk\ capacity},\mathrm{radiation\ capacity})$ at $(S_{\mathrm{BH}},N,n)$.
background
Gravity Track 3.C derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation fraction $t\in[0,1]$ shrinks bulk capacity as $S_{\mathrm{BH}}(1-t)$ and grows radiation capacity as $S_{\mathrm{BH}}t$. Purity of the joint bulk⊗radiation state plus Schmidt balance forces radiation entropy to saturate $\min$ of those two capacities, which is the triangle peaking at half evaporation.
The parent interface packages a closed bulk-radiation ledger, nonnegative $S_{\mathrm{BH}}$, a positive finite tick budget, a reversible linear tick operator, and an initial state, without yet tying entropy to that evolution. The ledger-tick Page curve is defined as the pointwise minimum of remaining-bulk and emitted-radiation capacities at the tick-induced evaporation fraction.
This structure is the remaining structural bridge: it attaches an explicit radiation-entropy-at-tick map and requires it to match that ledger-tick curve on the process budget.
proof idea
Definitional structure, not a proved theorem. It extends the operator Page process, adding a real-valued radiation entropy map on natural-number ticks and a single field asserting equality with the ledger-tick Page curve for every $n\le N$. Inhabiting instances (e.g. the canonical witness) supply concrete fields; downstream lemmas rewrite via the equality field and apply endpoint identities of the ledger-tick curve (zero at full evaporation, etc.).
why it matters
Closes the operator-layer surface for Track 3.C: carrier, unitary tick, iterated evolution, and entropy readout linked to the derived triangular curve. Downstream, the master-theorem handoff endpoint requires nonemptiness of this readout on a toy bulk-radiation pair; the one-statement operator interface theorem and the operator-process certificate both list it as a conjunct; the canonical witness proves the interface is inhabited via an identity tick. Sibling lemmas (radiationEntropyAtTick at zero, full, and page fraction) discharge concrete curve values through the equality field.
Framework role: structural, not dynamical closure. The module status is zero-sorry structural theorem for the min-capacity derivation; this readout still does not derive entropy from a microscopic Hamiltonian or recognition update. That gap is stated explicitly on the one-statement theorem and remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.