IsManyBodyAmplitudeLinear
plain-language theorem explainer
Amplitude-linearity for a many-body channel map means the map coincides pointwise with some complex-linear endomorphism of the macroscopic channel ledger on a finite site family. Anyone citing the Track 2.C many-body lift or the master-theorem Fork C endpoint uses this predicate as the target property. The body is a pure Prop definition: existence of a LinearMap witness equal to the response on every ledger state.
Claim. Let $\iota$ be a finite type of channel sites and let $R$ map the many-body macroscopic channel ledger on $\iota$ to itself. Then $R$ is many-body amplitude-linear if there exists a $\mathbb{C}$-linear endomorphism $L$ of that ledger such that $R(\Psi)=L(\Psi)$ for every ledger state $\Psi$.
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 on that carrier, and operational channel observables arise by substrate-local prepare-apply-extract-calibrate access. Composition of those linear pieces forces the binary physical channel response to be amplitude-linear.
The many-body ledger is the macroscopic ledger over a finite index type $\iota$ of channel sites (the sitewise $\mathrm{PiTensorProduct}$ lift of the binary channel). A response $R$ on that ledger is the many-body object whose structural property this definition names: agreement with some $\mathbb{C}$-linear endomorphism, not merely a set-theoretic self-map.
This is the many-body counterpart of the binary amplitude-linearity predicate used throughout the same module. Downstream theorems assert the property for sitewise families of binary physical responses; the definition itself only packages the Prop.
proof idea
Definition, not a proved theorem. The body is the standard existential packaging: there exists $L$ of type linear endomorphism of the many-body ledger over $\mathbb{C}$ such that $R$ and $L$ agree on every state. No tactics, no upstream lemmas are applied inside the definition; witnesses are supplied later by theorems such as the sitewise many-body lift.
why it matters
This predicate is the target of the many-body Track 2.C closure. The theorem manyBodyPhysicalChannelResponse_isAmplitudeLinear and the one-statement package T0T8_many_body_physical_channel_amplitude_linear_one_statement both conclude it for any finite sitewise family of binary physical channel responses. The certificate structure ManyBodyPhysicalChannelAmplitudeLinearCert records the same conclusion as a field, and the master-theorem handoff Track2ManyBodyEndpoint (Fork C) is literally quantified as inducing this property on the many-body ledger, together with sitewise action on pure tensors and inheritance of the local density-only collapse.
In the framework chain it sits after T0-T8 substrate semantics (joint carrier from T7, joint linearity from the Schrödinger-derivation lift, substrate-local observables) have already forced binary amplitude-linearity; the many-body definition is the language in which that binary closure is lifted. It does not itself discharge density-only no-go hypotheses; those ride on the theorems that inhabit the predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.