canonicalCyclicJointOperator
plain-language theorem explainer
The canonical joint operator on the binary-tensor substrate is the tensor product of the single-tick cyclic shift with itself. It is a concrete nonempty witness: a ℂ-linear endomorphism of the joint matter-channel space that factorizes through recognition updates on both factors. Gravity-track forcing and no-go theorems cite it as default T0–T8 substrate dynamics. The body is simply TensorProduct.map of the two cyclic-shift linears.
Claim. Let $U:\mathrm{Signal}_8\to_{\mathbb{C}}\mathrm{Signal}_8$ be the single-site cyclic-shift recognition update (the unique $\mathbb{C}$-linear one-tick update on the eight-tick ledger). The canonical cyclic joint operator is the $\mathbb{C}$-linear endomorphism $R_J=U\otimes U$ of the joint substrate $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$.
background
Track 2.C closes the substrate side of the amplitude-linearity forcing. Sessions 85–86 gave a single-factor dichotomy (amplitude-linear and density-only forces the zero map) and a joint lift: any ℂ-linear joint response that factorizes on pure tensors through a nontrivial matter response forces the channel factor to be amplitude-linear. Those results assumed factorization; this module plugs in actual substrate dynamics.
The matter-side dynamics is the cyclic shift on Signal8 (eight-tick octave ledger), packaged as the ℂ-linear map cyclicShiftLinear from the macroscopic ledger. Linearity comes from additivity and scalar homogeneity of the shift in the Schrödinger-derivation layer. The joint substrate is the binary tensor product of two such signal spaces (matter × channel).
Upstream, cyclicShiftLinear is exactly that packaged endomorphism. The present definition lifts it to the joint space by applying the same update independently on each tensor factor.
proof idea
Definitional, not a proof. The body is one constructor application: TensorProduct.map of cyclicShiftLinear with itself. That yields a ℂ-linear endomorphism of the joint substrate whose action on elementary tensors is $(U\otimes U)(\psi\otimes\varphi)=U\psi\otimes U\varphi$. No tactics; Mathlib supplies the tensor-product linear-map API.
why it matters
This is the concrete witness that the forcing hypothesis space is inhabited. Downstream, the pure-tensor factorization theorem records that the operator factors through the recognition update on both sides. canonicalRecognitionFactorization packages operator plus both factor maps into the factorizable-joint structure used by certificates.
In the physical-channel layer it is abbreviated as canonical T0–T8 joint dynamics: independent recognition on each factor, joined by the substrate tensor. That feeds the unconditional no-go: under T0–T8 substrate semantics, no joint dynamics admits a nontrivial density-only physical channel response. Substrate-local-access theorems use it to show the operator arises from a recognition probe, making the access proposition non-vacuous and closing the cert chain from access to section readout to amplitude-linearity.
Framework landmarks: T7 eight-tick octave (the Signal8 carrier) and the recognition update as single-tick dynamics; the joint lift is the gravity-track bridge from ledger dynamics to channel response.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.