JointSubstrate
plain-language theorem explainer
The joint matter-plus-channel substrate is the binary tensor product of two eight-slot signal ledgers over the complex numbers. Matter occupies the first factor and the channel the second. Anyone proving amplitude-linear forcing or density-only collapse on the joint ledger cites this type. The declaration is a one-line type synonym.
Claim. Define the joint substrate as $S_8 \otimes_{\mathbb{C}} S_8$, where $S_8$ is the eight-component complex signal ledger. The first factor is the matter ledger and the second is the channel ledger.
background
Session 85 closed a single-factor dichotomy on the eight-slot signal ledger: no nontrivial channel response is both amplitude-linear and density-only. Track 2.C lifts that dichotomy to a joint matter-plus-channel setting.
The joint substrate is modelled as the algebraic tensor product of two copies of the signal ledger over $\mathbb{C}$. The first factor carries matter degrees of freedom; the second carries channel degrees of freedom. Pure tensors $\psi \otimes \varphi$ are the elementary joint states on which factorized responses act separately.
The module works entirely inside this binary-tensor model. Downstream lemmas extract or insert factors via the universal property of the tensor product, then reduce joint claims to single-factor amplitude-linearity.
proof idea
One-line type abbreviation: the joint substrate is defined to be the Mathlib tensor product of two copies of the eight-slot signal type over $\mathbb{C}$. No proof obligations.
why it matters
This type is the ambient space for the entire Track 2.C joint-substrate lift. It is the carrier of pure-tensor factorization, the factor-extraction maps, and the closure theorem that a density-only channel response with nontrivial matter coupling must vanish.
Downstream, FactorizableJointSubstrate packages a joint linear operator together with matter and channel responses linked by pure-tensor factorization on this type. The Track 2.C closure step composes that factorization with the Session 85 single-factor dichotomy to rule out nontrivial CPTP-classical channel readouts under matter coupling. The many-body handoff endpoint quantifies over families of operators on this same joint substrate and inherits the local density-only collapse.
Full paper-IV Track 2 upgrade from model to theorem still needs the joint recognition operator to be $\mathbb{C}$-linear via the single-factor Schrödinger lift; this abbreviation supplies the type on which that lift acts. It sits in the gravity quantum-channel line that ultimately feeds the eight-tick octave structure (T7) into many-body amplitude linearity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.