isAmplitudeLinear_channel_of_recognitionUpdate
plain-language theorem explainer
If a complex-linear joint operator on the binary tensor substrate factorizes on pure tensors with the cyclic-shift recognition update on the matter factor, the channel factor must be amplitude-linear. Gravity Track 2.C cites this as the substrate-side forcing step that upgrades paper IV's T2 from model to theorem (modulo factorization). The proof obtains nontriviality of the recognition update and feeds it into the Session 86 joint-substrate lift.
Claim. Let $R_J$ be a $\mathbb{C}$-linear endomorphism of the joint substrate and $R_C$ a map on the eight-tick signal space. If $R_J$ factorizes on pure tensors as the product of the substrate recognition update (cyclic shift) on the matter factor with $R_C$ on the channel factor, then $R_C$ is amplitude-linear.
background
Track 2.C closes the gravity quantum-channel argument on the binary tensor substrate $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$. Session 85 gave the single-factor dichotomy: a map that is both amplitude-linear and density-only must vanish. Session 86 lifted that to the joint setting: if a $\mathbb{C}$-linear joint operator $R_J$ factorizes on pure tensors through factor maps $R_M$ and $R_C$, and $R_M$ is nontrivial, then $R_C$ is amplitude-linear.
This module instantiates the matter factor with the actual substrate dynamics. The recognition update is the unique $\mathbb{C}$-linear single-tick cyclic shift on $\mathrm{Signal}_8$ (the discrete time-evolution generator $T$ with $(Tf)(k)=f(k+1\bmod 8)$), packaged from the Schrödinger derivation and macroscopic ledger. Nontriviality is witnessed by the shift sending the zero mode at index 0 to a nonzero value.
Amplitude-linearity means the channel responds linearly in field amplitude rather than only through densities. Pure-tensor factorization is the structural hypothesis that $R_J(\psi\otimes\phi)$ splits as a product of independent matter and channel actions; it remains an assumption on general endomorphisms of the joint space.
proof idea
Term-mode, two steps. First unpack recognitionUpdate_nontrivial to obtain a witness pair $(\psi_0,i_0)$ showing the cyclic-shift recognition update is a nontrivial matter map. Then apply the Session 86 joint-substrate lift isAmplitudeLinear_channel_of_pureTensorFactorization, specializing the matter factor to the recognition update and feeding in the pure-tensor factorization hypothesis together with that nontriviality witness. No further algebraic work: the lift already carries the forcing from joint $\mathbb{C}$-linearity plus factorization down to amplitude-linearity of the channel factor.
why it matters
This is the substantive Track 2.C substrate-side forcing step in the binary-tensor model. It feeds directly into the Track 2.C master theorem track2C_channel_isAmplitudeLinear, which states that under a recognition-coupled factorizable joint substrate the channel-side response is amplitude-linear, and into the closure theorem channel_eq_zero_of_density_only_of_recognitionUpdate, which composes with Session 85's dichotomy to kill density-only channel responses under substrate matter dynamics.
In paper-IV language this upgrades T2 from MODEL to THEOREM inside the binary-tensor model, modulo pure-tensor factorization. The eight-tick octave (T7) enters because the recognition update is the cyclic shift on $\mathrm{Signal}_8$. The remaining open piece, flagged in the module doc, is deriving factorization itself from substrate axioms: a general $\mathbb{C}$-linear endomorphism of $\mathrm{Signal}_8\otimes\mathrm{Signal}_8$ need not factor, and that derivation is the next subsession.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.