BulkRadiationLedger
plain-language theorem explainer
Closed bulk–radiation carrier for the dynamical Page process: the ℂ-tensor product of a finite bulk ledger with a Hawking-radiation ledger. Track 3.C operator-level work cites it as the joint state space on which unitary ticks act. The declaration is a one-line type abbreviation, not a proved claim.
Claim. For finite index types $\beta$ and $\rho$, the bulk–radiation ledger is the tensor product space $H_{\mathrm{bulk}}(\beta)\otimes_{\mathbb{C}} H_{\mathrm{rad}}(\rho)$, where $H_{\mathrm{bulk}}$ is the macroscopic ledger over remaining black-hole degrees of freedom and $H_{\mathrm{rad}}$ is the macroscopic ledger over emitted Hawking radiation.
background
Module Gravity.PageCurveDynamical (Track 3.C) 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$. A pure joint state on bulk $\otimes$ radiation forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$, which saturates to the triangular curve.
BulkLedger β is the finite macroscopic Signal8 ledger on remaining black-hole degrees of freedom; the radiation side is the analogous ledger on emitted quanta. The closed carrier is their tensor product over $\mathbb{C}$, the Lean-facing substrate Track 3.C requests for operator-level Page ticks.
RS time is discrete in ticks ($\tau_0=1$); the eight-tick octave is the fundamental evolution period. This abbrev only names the joint Hilbert-space type; unitary tick data and entropy readout sit on top of it.
proof idea
Definitional abbreviation only: expand to the Mathlib tensor product BulkLedger β ⊗[ℂ] HawkingRadiationLedger ρ. No tactics, no lemmas, no proof obligations. Finite-type and decidable-equality instances are inherited so the carrier is a finite-dimensional complex vector space suitable for linear maps.
why it matters
Gives Track 3.C an explicit joint carrier so the Page process is no longer a kinematic ansatz. Downstream, PageTickUnitary is a reversible ℂ-linear tick (and inverse) on this carrier; stateAfterOperatorTicks iterates that tick; OperatorPageProcess packages carrier, initial state, tick, and evaporation budget. The one-statement interface and PageCurveOperatorProcessCert assert nonemptiness of this carrier together with unitary tick and entropy readout. Master-theorem handoff exposes the same bundle as Track3OperatorProcessEndpoint.
Framework role: closes the structural gap between Session 101's hand-drawn triangle and a substrate where unitarity plus Schmidt balance force $S_{\mathrm{rad}}=\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$. Open: deriving the entropy readout from a specific microscopic Hamiltonian or recognition update (explicitly not master-clause readiness).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.