ManyBodyChannelLedger
plain-language theorem explainer
Aliases the many-body channel ledger to the macroscopic ledger: a finite tensor product of eight-tick signal spaces, one factor per channel site. Gravity Track 2.C cites it when stating amplitude-linearity for multi-site physical channel responses. The body is a one-line type synonym for MacroscopicLedger.
Claim. For a finite index type $\iota$ with decidable equality, the many-body channel ledger is the type $\bigotimes_{i\in\iota}\mathrm{Signal}_8$ of complex tensor products of eight-tick signal spaces, one factor per channel site.
background
Track 2.C closes unconditional amplitude-linearity of physical channel responses from T0–T8 substrate semantics alone. The joint substrate is $\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$ (T7 eight-tick factors), joint dynamics is $\mathbb{C}$-linear, and operational channel observables arise by substrate-local prepare–evolve–extract access.
The macroscopic ledger is already defined as $\bigotimes[\mathbb{C}]_{_:\iota}\mathrm{Signal}_8$: one eight-tick factor per site in a finite family $\iota$. Recognition updates act factorwise by the linearized cyclic shift. This abbrev simply renames that carrier for the many-body channel setting, so multi-site responses can be stated as maps on a single ledger type rather than ad hoc products.
Upstream anchors $A$ (active edges per tick) and double-slit amplitude appear only as ambient RS vocabulary; the type itself depends only on the macroscopic ledger construction.
proof idea
Pure definitional synonym: the body is the identifier MacroscopicLedger ι under the same finite-type and decidable-equality hypotheses. No proof obligations, no lemmas applied.
why it matters
Gives the carrier type for the multi-site half of Track 2.C. Downstream, IsManyBodyAmplitudeLinear says a response $R$ is amplitude-linear when it agrees with some $\mathbb{C}$-linear endomorphism of this ledger. The sitewise construction manyBodyPhysicalChannelLinearMap builds that endomorphism from local physical-channel data (PhysicalChannelResponseOf at each $i$), and manyBodyPhysicalChannelResponse is the corresponding function view.
Together these lift the single-channel unconditional closure (joint linearity plus substrate-local access implies amplitude-linearity) to a finite family of channel sites, still without density-only hypotheses. Framework landmarks in play: T7 eight-tick octave on each factor, and the Schrödinger-derived $\mathbb{C}$-linearity of joint dynamics on the T0–T8 substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.