operator_level_page_process_structural_prop
plain-language theorem explainer
Defines the structural proposition that the operator-level Page process is inhabited: there exists a bulk-radiation carrier with reversible tick dynamics and a Page-entropy readout matching the ledger curve. Gravity auditors cite it as the interface certificate for the dynamical (non-ansatz) Page curve. The body is a one-line Nonempty assertion on the unit finite types.
Claim. The proposition that there exists an operator-level Page entropy readout on one-element bulk and radiation index types: a reversible tick process on the bulk-radiation carrier together with a radiation-entropy function of tick count that equals the triangular Page curve for every admissible tick.
background
Module Gravity.PageCurveDynamical derives the triangular Page curve from Schmidt-balanced ledger dynamics rather than postulating it. Evaporation is parameterized by $t \in [0,1]$; bulk capacity falls as $S_{BH}(1-t)$ and radiation capacity rises as $S_{BH}, t$. Purity of the joint bulk $\otimes$ radiation state plus Schmidt's theorem force equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}}, \log d_{\mathrm{rad}})$, which saturates to the triangular curve under maximal entanglement.
The upstream structure OperatorPageEntropyReadout packages that story at the operator layer: it extends the operator Page process by a radiation-entropy-at-tick map and the equality that this readout matches the ledger-tick Page curve for every tick up to the total. The present definition simply names the proposition that this interface is inhabited on the smallest finite types $(\mathrm{Fin},1,\mathrm{Fin},1)$.
proof idea
Definitional, not a proof. The proposition is literally the assertion that the type of operator Page entropy readouts on unit bulk and radiation index sets is nonempty. No tactics or lemmas are applied here; inhabitation is discharged downstream by exhibiting the canonical readout constructor.
why it matters
This is the named structural gate for Track 3.C's operator layer. Session 101 only had a kinematic triangular ansatz; this module replaces that ansatz by a derived $\min$ of bulk and radiation capacities. The proposition records that the explicit carrier, reversible tick operator, and entropy readout are jointly inhabited, so the dynamical recipe is not vacuous.
Its sole consumer is the certificate theorem that the proposition holds, proved by feeding the canonical operator readout at total ticks $1$ with trivial positivity side conditions. That certificate closes the operator-level interface for the Page curve without RS-internal axioms. In the broader Recognition gravity track it sits under the macroscopic ledger and master theorem imports, tying unitary evaporation dynamics to the ledger-tick Page shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.