canonicalCyclicJointOperator_pureTensorFactorization
plain-language theorem explainer
The canonical joint operator on the binary-tensor substrate, built as the tensor product of two cyclic-shift maps, acts on pure tensors by applying the single-factor recognition update to each leg. Gravity-track authors cite it to discharge the pure-tensor factorization hypothesis of the Session 86 joint-substrate lift. The proof is a one-step rewrite by the universal property of TensorProduct.map on elementary tensors.
Claim. Let $R_J$ be the canonical joint operator $\mathrm{map}(\mathrm{cyclic\_shift},\mathrm{cyclic\_shift})$ on the joint substrate $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$, and let $R$ be the single-factor recognition update (cyclic shift on $\mathrm{Signal}_8$). Then for all pure tensors $\psi\otimes\varphi$, one has $R_J(\psi\otimes\varphi)=(R\psi)\otimes(R\varphi)$.
background
Track 2.C closes the substrate side of the amplitude-linear forcing argument. Sessions 85–86 proved a single-factor dichotomy (amplitude-linear and density-only forces the zero map) and a joint lift: a $\mathbb{C}$-linear joint operator that factorizes on pure tensors through a nontrivial matter response forces the channel response to be amplitude-linear. Both results were conditional on pure-tensor factorization.
Pure-tensor factorization means a joint endomorphism $R_J$ satisfies $R_J(\psi\otimes\varphi)=(R_M\psi)\otimes(R_C\varphi)$ for all single-factor states; physically, the joint ledger is a tensor product of matter and channel ledgers. The substrate recognition update is the cyclic shift on $\mathrm{Signal}_8$ (eight-tick octave dynamics from the Schrödinger derivation). The canonical joint operator is the concrete $\mathbb{C}$-linear map $\mathrm{TensorProduct.map}$ of two copies of the linear cyclic shift, witnessing that the forcing hypothesis space is nonempty.
proof idea
Fix pure tensors $\psi,\varphi$. Unfold the claim to equality of $R_J(\psi\otimes\varphi)$ with $(R\psi)\otimes(R\varphi)$. Because $R_J$ is defined as $\mathrm{TensorProduct.map}$ of the two linear cyclic shifts, rewrite by TensorProduct.map_tmul, which states that the map sends elementary tensors to the pair of images. The remaining identity is definitional: the linear cyclic-shift maps agree with the function-level recognition update on each factor, so rfl closes.
why it matters
This lemma is the concrete factorization witness that makes Track 2.C non-vacuous. Downstream, canonicalRecognitionFactorization packages $R_J$, both factor responses, and this proof into a single factorizable joint substrate record used by the certification layer. Separately, canonicalCyclicJointOperator_arisesFromRecognitionProbe applies the factorization (with a nonzero probe state) to show the canonical operator arises from recognition-probe substrate access, so the access proposition is inhabited.
In the broader Recognition chain the cyclic shift is the unique $\mathbb{C}$-linear single-tick update on the eight-tick octave (T7). Establishing that the joint dynamics factor through that update on both legs lets the Session 86 lift force amplitude-linearity of any channel response coupled to substrate matter, and rules out nontrivial density-only channels under the same dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.