BulkLedger
plain-language theorem explainer
Names the finite bulk carrier for evaporating black-hole degrees of freedom as a macroscopic eight-tick Signal ledger on a finite index type. Gravity Track 3.C cites it whenever bulk Hilbert-space capacity, tick evolution, or the closed bulk–radiation tensor product is written. The body is a one-line type synonym for the macroscopic ledger.
Claim. For a finite index type $\beta$ with decidable equality, the bulk ledger is the macroscopic ledger $\bigotimes_{i\in\beta}\mathrm{Signal}_8$ over the remaining black-hole degrees of freedom.
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_{\mathrm{BH}}(1-t)$ while radiation capacity rises as $S_{\mathrm{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 Page triangle.
The upstream macroscopic ledger is the finite tensor product $\bigotimes[\mathbb{C}]_{i\in\iota}\mathrm{Signal}_8$. Each factor carries the linearized cyclic eight-tick shift; the bulk synonym simply specializes that carrier to the remaining black-hole index set $\beta$.
proof idea
Definitional abbreviation only: expand to MacroscopicLedger.MacroscopicLedger β. No proof obligations, tactics, or lemmas.
why it matters
Supplies the Lean-facing bulk half of Track 3.C's closed carrier. Downstream, BulkRadiationLedger tensors it with the Hawking-radiation ledger; tick operators and stateAfterOperatorTicks_succ act on that product. The MasterTheorem handoff consumes the resulting capacity identities in track3_tick_capacity_endpoint_holds (Fork D endpoint). Together with the radiation twin and the capacity-sum invariant, it turns the kinematic Page ansatz of Session 101 into a derived $\min$ of two monotone ledger capacities under unitarity and Schmidt balance, consistent with the eight-tick octave substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.