MacroscopicLedger
plain-language theorem explainer
The macroscopic ledger Hilbert carrier is the finite tensor product over ℂ of single-site eight-tick signal spaces, one factor per site. Anyone working multi-site ledger superposition or the gravity-channel recognition update cites this type. It is a direct abbreviation of Mathlib's PiTensorProduct, not a proved statement.
Claim. For a finite indexing set $\iota$ of sites, the macroscopic ledger Hilbert carrier is the $\iota$-fold tensor product over $\mathbb{C}$ of the single-site eight-tick analytic signal carriers: $\bigotimes_{i\in\iota}^{\mathbb{C}} \mathrm{Signal}_8$.
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a paper-level conditional claim to a structural Lean object. The single-site carrier is the eight-tick analytic signal space (identified with the forced Signal8 from complex-structure forcing), on which the recognition update is the linearization of the cyclic eight-tick shift. That single-site map is already proved ℂ-linear in the Ledger Superposition module.
The eight-tick period is the fundamental RS evolution octave (T7): one tick is the RS-native time quantum τ₀ = 1. Macroscopic configurations are multi-site pure tensors and their finite linear combinations. The ambient construction is Mathlib's PiTensorProduct over ℂ, so the type inherits the universal property of the algebraic tensor product of modules.
This module only sets the carrier type. The recognition update on it is defined separately as the factor-wise map of the single-site cyclic shift.
proof idea
Pure definitional abbreviation: the type is Mathlib's finite Pi-tensor product ⨂[ℂ] _ : ι, Signal8. No tactics, no lemmas, no sorry. Downstream objects (MacroscopicShift, the certificate structure) inherit ℂ-linearity from PiTensorProduct.map applied to the already-linear single-site cyclic shift.
why it matters
Paper IV's Theorem 1 (Ledger Superposition) is unconditional at one site. Multi-site physicality of ledger superpositions needs the same statement at tensor-product level; this carrier is the type on which Track 2.A discharges that upgrade from conditional to structural theorem (0 sorry, 0 RS-internal axiom).
It is the domain and codomain of the macroscopic recognition update (MacroscopicShift), which is the Pi-tensor map of the single-site cyclic shift. That map feeds the five-clause certificate MacroscopicLedgerTheorem (single-site linearity, pure-tensor action, additivity, scalar homogeneity, finite superposition) and the inhabitation theorem that the certificate is nonempty for every finite site set. Downstream gravity work also reuses the type as the bulk and Hawking-radiation ledgers in the dynamical Page-curve module.
Framework landmarks: T7 eight-tick octave as the single-site factor; the construction does not yet identify the update with the gravitational-channel response (Track 2.C).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.