track2C_channel_eq_zero_of_density_only
plain-language theorem explainer
Under a recognition-coupled factorizable joint substrate, any density-only channel response is forced to the zero map on eight-tick signals. Gravity and quantum-channel workers cite this for Track 2.C closure and the no-classical-mediator theorem. The proof rewrites the matter factor as the substrate recognition update, obtains pure-tensor factorization, and applies the substrate-side zero lemma.
Claim. Let $F$ be a recognition-coupled factorizable joint substrate: a $\mathbb{C}$-linear joint operator on $\mathrm{Signal}_8\otimes_{\mathbb{C}}\mathrm{Signal}_8$ that factorizes on pure tensors, with matter factor equal to the substrate recognition update. If the channel response $R_C$ is density-only (invariant under multiplication by unit-modulus complex scalars), then $R_C(\varphi)=0$ for every eight-tick signal $\varphi$.
background
Track 2.C aggregates Sessions 85–87 on the binary-tensor model. The joint substrate is $\mathrm{Signal}8\otimes{\mathbb{C}}\mathrm{Signal}_8$. Pure-tensor factorization means the joint operator acts as $R_J(\psi\otimes\varphi)=(R_M\psi)\otimes(R_C\varphi)$. A recognition-coupled factorization further fixes the matter factor: $R_M$ equals the substrate recognition update (projector-after-shift), as forced by the T0–T8 chain and single-site Schrödinger linearity.
Density-only is the structural footprint of a CPTP-classical density-matrix readout: $R(c\cdot\psi)=R(\psi)$ whenever $|c|=1$. Amplitude-linear responses are instead phase-equivariant. Session 85 already shows no nontrivial single-factor map is both amplitude-linear and density-only; Sessions 86–87 lift the dichotomy through factorization to the joint setting.
The local master claim is that under recognition-coupled factorization the channel side must be amplitude-linear, so any density-only candidate collapses to zero. That upgrades paper IV's T2 from a modeling choice to a structural theorem conditional on the factor-product axiom.
proof idea
Tactic proof in two steps. First build a pure-tensor factorization hypothesis for the joint operator with matter factor equal to the recognition update: take the structure's factorization field and rewrite the matter side via the recognition-coupling equality $R_M=$ recognition update. Second, apply the substrate lemma channel_eq_zero_of_density_only_of_recognitionUpdate, which already proves that under pure-tensor factorization through the recognition update, density-only forces the channel map to vanish on every signal. No further case analysis.
why it matters
This is the density-only half of the Track 2.C master certificate. It is the body of track2C_headline (channel amplitude-linear and density-only implies zero), the engine of the existence-form no-go (no recognition-coupled factorization with a nontrivial density-only channel), and the direct callee of Track 2.D's no_classical_mediator_under_T0T8. The cert inhabitant wires it as density_only_impossible.
In framework terms it closes the CPTP-classical escape route for gravity mediation on the eight-tick octave: once matter is locked to the T0–T8 recognition update and the joint operator factorizes, a density-matrix-only channel cannot carry nontrivial response. Paper IV's T2 is thereby forced from substrate structure rather than postulated as a model tag, conditional on the named factorizable joint-substrate axiom.
The remaining open lift is unconditional Track 2.C without pure-tensor factorization: either rederive factorization from a stricter substrate axiom or eliminate it. Until that lift, the result is structural but not fully unconditional theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.