HawkingRadiationLedger
plain-language theorem explainer
Names the finite Hawking-radiation side of the Page process as a macroscopic Signal8 ledger indexed by radiation degrees of freedom. Anyone building the bulk⊗radiation joint carrier or the dynamical Page curve cites this type alias. It is a one-line abbreviation of the existing macroscopic ledger construction.
Claim. For a finite index type $\rho$ with decidable equality, the Hawking-radiation ledger is the macroscopic ledger $\bigotimes_{i\in\rho}\mathrm{Signal}_8$ over emitted radiation degrees of freedom.
background
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_{\mathrm{BH}}(1-t)$ while radiation capacity grows as $S_{\mathrm{BH}},t$. Unitary evolution from a pure bulk state keeps the joint bulk⊗radiation state pure, so Schmidt forces equal reduced entropies bounded by $\min(\log d_{\mathrm{bulk}},\log d_{\mathrm{rad}})$.
The macroscopic ledger is the finite tensor product $\bigotimes[\mathbb{C}]_{i\in\iota}\mathrm{Signal}_8$ of eight-tick recognition registers. The sibling bulk ledger is the same construction over remaining black-hole indices. This abbreviation supplies the radiation factor of that pair, so the closed carrier can be written as a Hilbert-space tensor product of two macroscopic ledgers.
proof idea
Pure definitional abbreviation: the type is identified with MacroscopicLedger at the radiation index type $\rho$. No proof obligations; instances of Fintype and DecidableEq are inherited from the parameter.
why it matters
Feeds BulkRadiationLedger, the closed bulk–radiation carrier requested by Track 3.C: bulk ledger tensor Hawking-radiation ledger over $\mathbb{C}$. That joint type is the substrate on which reversible tick operators act and from which pageCurveFromLedgerTicks and the capacity-sum invariant extract the triangular Page curve as $\min(\mathrm{bulkCapacity},\mathrm{radiationCapacity})$.
In the Recognition framework this is the radiation half of the finite eight-tick ledger geometry underlying holographic entropy bookkeeping. It does not itself force $D=3$ or the J-cost; it only names the radiation register so dynamical unitarity can produce the Page peak at $t=1/2$ without a kinematic ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.