not_exists_density_only_channel_with_recognitionUpdate
plain-language theorem explainer
No ℂ-linear joint operator on the binary-tensor substrate factorizes through the cyclic-shift recognition update on matter and a nontrivial density-only channel map. Track 2.C gravity cites this as the existence-form no-go closing the substrate-side dichotomy. Proof is a one-line contradiction via the zero-channel lemma under density-only plus pure-tensor factorization.
Claim. There do not exist a $\mathbb{C}$-linear endomorphism $R_J$ of the joint substrate and a map $R_C$ on the eight-tick signal space such that $R_J$ factorizes on pure tensors through the recognition update and $R_C$, $R_C$ is density-only, and $R_C$ is not identically zero.
background
Gravity Track 2.C closes the substrate side of the amplitude-linear versus density-only dichotomy for quantum channels. Session 85 proved the single-factor dichotomy: a response that is both amplitude-linear and density-only must vanish. Session 86 lifted this to the joint substrate: if a ℂ-linear joint operator factorizes on pure tensors through a nontrivial matter response and a channel response, then the channel factor is forced to be amplitude-linear.
This module instantiates the matter factor by the actual substrate dynamics: the unique ℂ-linear single-tick recognition update on Signal8 (cyclic shift). The joint space is the binary tensor model. Pure-tensor factorization means the joint map acts as the product of the two factor responses on elementary tensors. Density-only marks channel maps that respond only to density, not amplitude. The nontriviality hypothesis of the Session 86 lift is discharged by the substrate update itself (shift sends the zero basis vector to a nonzero one).
proof idea
Term-mode proof by contradiction. Unpack the existential into a joint operator $R_J$, a channel $R_C$, a pure-tensor factorization hypothesis through the recognition update, a density-only hypothesis, and a witness signal $\varphi$ with $R_C\varphi\neq 0$. Apply channel_eq_zero_of_density_only_of_recognitionUpdate (Session 86 amplitude-linear forcing under the recognition update, composed with the Session 85 dichotomy) to conclude $R_C\varphi=0$, contradicting the witness. One-line reduction; no extra algebraic work.
why it matters
Existence-form no-go of Track 2.C substrate-side closure: a density-only channel cannot participate nontrivially in any joint recognition operator that factorizes through cyclic-shift matter dynamics. Paired with the forcing that any such channel factor is amplitude-linear, and with the zero lemma for density-only responses, it seals the dichotomy on the binary-tensor model. The eight-tick signal space is the T7 octave from the unified forcing chain. No recorded downstream consumers yet; the companion canonical cyclic joint operator shows the amplitude-linear side of the hypothesis space is inhabited, so the no-go is sharp rather than vacuous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.