operator_page_process_interface_one_statement
plain-language theorem explainer
On the one-mode bulk–radiation carrier, the operator Page interface is inhabited: a closed ledger, a reversible ℂ-linear tick, and an entropy readout whose radiation entropy vanishes at the start and end of evaporation. States advance exactly by applying the unitary tick. Gravity Track 3.C and the MasterTheorem handoff cite this as the operator-process endpoint. The proof is a single term packing inhabitance witnesses with the structure field equalities.
Claim. There exist a bulk–radiation ledger on $\mathrm{Fin}\,1\otimes\mathrm{Fin}\,1$, a reversible $\mathbb{C}$-linear Page tick on that carrier, and an operator entropy readout. For every operator Page process $P$ and every $n\in\mathbb{N}$, the state at tick $n+1$ equals the unitary tick applied to the state at tick $n$. For every such readout, radiation entropy is $0$ at tick $0$ and at the final tick budget.
background
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$\otimes$radiation state plus Schmidt balance forces radiation entropy to equal $\min$ of those two monotone bounds, which is the Page triangle peaking at $t=1/2$.
The bulk–radiation ledger is the tensor product carrier $\mathrm{BulkLedger}\otimes_{\mathbb{C}}\mathrm{HawkingRadiation}$. A Page tick unitary is a pair of mutually inverse $\mathbb{C}$-linear maps on that carrier (algebraic unitarity; metric inner-product preservation is deferred). An operator Page process packages nonnegative black-hole entropy $S_{\mathrm{BH}}$, a positive finite tick budget, a unitary tick, and an initial state. The entropy readout extends the process by a function $\mathbb{N}\to\mathbb{R}$ forced equal to the ledger-tick Page curve on $0\le n\le\mathrm{totalTicks}$.
This one-statement packages inhabitance of those interfaces on the minimal finite types $\mathrm{Fin},1$, plus the dynamical and boundary entropy laws the structures already carry.
proof idea
Term-mode packing of six conjuncts. The bulk–radiation ledger on $\mathrm{Fin},1$ is witnessed by the zero vector. Page-tick unitarity uses the inhabited instance pageTickUnitary_inhabited. The entropy-readout inhabitance is the upstream lemma operator_level_page_process_structural_prop_holds. The remaining three conjuncts are pointwise applications of structure fields: successor evolution via stateAtTick_succ, initial radiation entropy via radiationEntropyAtTick_zero, and terminal radiation entropy via radiationEntropyAtTick_full. No further rewriting.
why it matters
Closes the operator-process surface for Gravity Track 3.C: an explicit bulk$\otimes$radiation carrier, reversible linear tick, iterated dynamics, and a readout bridge to the ledger-tick Page curve. Downstream, track3_operator_process_endpoint_holds in MasterTheoremHandoffIntegration is literally this statement, so the integration lane consumes it as the Agent D / Track 3 operator endpoint.
In the RS gravity stack this sits above the structural min-of-capacities derivation of the Page triangle and below any claim that the readout equals a concrete microscopic recognition Hamiltonian. The module status is structural theorem (zero sorry). The doc-comment is explicit that master-clause readiness is not claimed: deriving the readout from a specific microscopic update remains open. Framework contact is the eight-tick / ledger time quantum only insofar as ticks parameterise evaporation; this declaration does not force $D=3$ or the $\alpha$ band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.