FactorizableJointSubstrate
plain-language theorem explainer
A named structural package for Track 2.C: a joint ℂ-linear operator on the binary tensor substrate together with matter and channel factor maps, plus a pure-tensor factorization witness. Gravity and quantum-channel workers cite it when fixing the master-plan axiom that matter and channel evolve independently at the operator level. As a structure definition there is no proof body; inhabitants supply the four fields.
Claim. A factorizable joint substrate consists of a $\mathbb{C}$-linear endomorphism $R_J$ of the joint substrate $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$, maps $R_M$ and $R_C$ on $\mathrm{Signal}_8$, and a pure-tensor factorization witness asserting $R_J(m \otimes c) = R_M(m) \otimes R_C(c)$ on elementary tensors. Equivalently, the joint response carries no cross-sector coherence between matter and channel factors.
background
Track 2.C in the gravity quantum-channel stack studies whether a gravitational channel response on the eight-tick ledger can be density-only or must be amplitude-linear. The binary-tensor model takes the joint substrate to be $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$ (matter ledger tensor channel ledger).
A general $\mathbb{C}$-linear endomorphism of that tensor product need not preserve product structure: the swap map is the standard counterexample that creates entanglement from pure tensors. The pure-tensor factorization condition forces the joint operator to act separately on each factor, so matter and channel sectors do not mix at the operator level.
The module aggregates Sessions 85–87: single-factor dichotomy on $\mathrm{Signal}_8$, joint lift under factorization, and substrate-side closure when the matter factor is the recognition update (cyclic shift). This structure is the named axiom packaging that factorization setup.
proof idea
Definitional structure with four fields and no proof obligations. An inhabitant must supply the joint linear map $R_J$, the matter and channel factor maps $R_M$ and $R_C$, and a term of type PureTensorFactorization witnessing that $R_J$ acts as $R_M \otimes R_C$ on pure tensors. Downstream constructions (for example the canonical cyclic-shift witness) fill these fields by naming concrete maps and an existing factorization lemma.
why it matters
This is the structural axiom that upgrades paper IV's Track 2.C from a MODEL tag toward a STRUCTURAL THEOREM in the binary-tensor setting. Downstream, RecognitionCoupledFactorization extends it by fixing the matter side to the substrate recognition update (cyclic shift), tying matter dynamics to the T0–T8 forcing chain. The canonical recognition-coupled factorization inhabits both layers with cyclic shift on each factor and the tensor-product joint map.
The physical-channel amplitude-linearity certificate uses this package to conclude that, under recognition-coupled factorization, a density-only channel response collapses to zero, so the gravitational channel must be amplitude-linear. The module doc is explicit that the fully unconditional lift (dropping the factor-product assumption on general joint operators) remains open; anti-retreat still wants that stronger closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.