canonicalOperatorPageEntropyReadout
plain-language theorem explainer
Canonical witness that the operator-level Page-entropy readout interface is inhabited. Given black-hole entropy S_BH ≥ 0 and positive tick count N, it packages the ledger-tick Page curve as radiation entropy under the identity tick unitary on trivial one-point bulk and radiation labels. Downstream structural inhabitation cites it. Built by direct field fill-in; the readout equality is reflexivity.
Claim. For any black-hole entropy $S_{\mathrm{BH}} \ge 0$ and any positive integer $N$, there is an operator Page-entropy readout on one-point bulk and radiation label spaces with entropy parameter $S_{\mathrm{BH}}$, total ticks $N$, identity tick unitary, zero initial state, and radiation entropy at tick $n$ equal to the ledger-tick Page curve of $(S_{\mathrm{BH}}, N)$ at $n$.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation fraction $t \in [0,1]$ splits total entropy between bulk and radiation capacities $S_{\mathrm{BH}}(1-t)$ and $S_{\mathrm{BH}} t$. Purity of the joint bulk⊗radiation state plus Schmidt balance forces radiation entropy to equal $\min$ of those capacities, which is the triangular curve peaking at half evaporation.
The structure being inhabited extends the operator Page process by a radiation-entropy-at-tick map and the requirement that this map agree with the ledger-tick Page curve on every admissible tick. That curve is the discrete sampling of the dynamical min-capacity formula along $N$ ticks.
The identity tick unitary on Fin 1 labels is only a formal reversible step: enough to show the interface type is nonempty, not a model of Hawking emission.
proof idea
Definitional constructor, not a tactic proof. Fields are filled directly: entropy and nonnegativity from the inputs; total ticks and positivity from $N$; tick unitary set to the identity page-tick unitary on one-point bulk and radiation; initial state zero; radiation entropy map set to the ledger-tick Page curve of $(S_{\mathrm{BH}}, N)$. The bridge equality (readout equals that Page curve at every tick $\le N$) is rfl because the map was defined to be exactly that function.
why it matters
Closes the operator-layer inhabitation obligation in Track 3.C. The sole downstream consumer is the structural proposition that the bulk-radiation carrier, reversible tick operator, and Page-entropy readout interface are inhabited; that theorem is a one-line package of this witness at unit entropy and one tick.
In the broader Recognition gravity stack this sits above the kinematic Session-101 ansatz: the triangular shape is already derived from Schmidt purification and capacity bounds, and this definition only certifies that an operator-facing readout type can point at that derived curve. It does not advance forcing-chain landmarks (T5–T8) or the RCL; it is interface glue between ledger ticks and the operator process certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.