track2C_headline
plain-language theorem explainer
Under a recognition-coupled factorizable joint substrate, the gravitational channel response is forced amplitude-linear, and any density-only (CPTP-classical) candidate collapses to the zero map. Gravity theorists citing paper IV Track 2.C as a structural (not model) result would quote this. The proof is a term-mode pair of the already-proved forcing and density-only-collapse lemmas in the same module.
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. Then the channel-side response $R_C$ is amplitude-linear (agrees with some $\mathbb{C}$-linear map), and if $R_C$ is density-only (invariant under unit-modulus phase rescaling) then $R_C\varphi = 0$ for every signal $\varphi$.
background
Track 2.C asks whether the gravitational channel response on the eight-tick ledger space $\mathrm{Signal}_8$ is forced to be amplitude-linear rather than a modeling choice. Amplitude-linear means the response agrees with some $\mathbb{C}$-linear map, so it preserves coherent superpositions. Density-only means invariance under $\psi \mapsto c\cdot\psi$ for $|c|=1$, the structural footprint of a CPTP-classical density-matrix readout.
The module aggregates Sessions 85–87. Session 85 gives the single-factor dichotomy: no nontrivial response is both amplitude-linear and density-only. Session 86 lifts to joint operators on $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$ that factorize on pure tensors. Session 87 closes the substrate side when the matter factor is the recognition update.
A recognition-coupled factorization is a factorizable joint substrate whose matter factor equals that recognition update (cyclic_shift). The T0–T8 forcing chain fixes matter dynamics to this update via single-site Schrödinger linearity, so the hypothesis is the master-plan constraint rather than an extra free choice.
proof idea
Term-mode pair constructor. The first conjunct is track2C_channel_isAmplitudeLinear F: under recognition-coupled factorization, joint linearity of $R_J$ plus pure-tensor factorization and the fixed matter update propagate amplitude-linearity to the channel factor. The second conjunct is the function fun hDen φ => track2C_channel_eq_zero_of_density_only F hDen φ, which applies the density-only impossibility lemma: any density-only channel response under the same hypothesis is forced to zero on every signal. No new algebra; the headline only packages the two closures.
why it matters
This is the binary-tensor Track 2.C master theorem: paper IV's T2 upgraded from MODEL to STRUCTURAL THEOREM under the named factor-product joint-substrate axiom. Downstream, amplitude_linear_forced_canonical_prop_holds instantiates it on the canonical witness; amplitude_linear_forced_one_statement packages it with the inhabited unconditional-hypothesis witness into the Track 2.C/2.D structural one-statement; amplitudeLinearForcedStructuralCert records both conjuncts in the structural certificate bundle.
Framework landmarks: the matter factor is pinned by the T0–T8 chain (eight-tick octave on $\mathrm{Signal}_8$, single-site linearity forcing cyclic_shift). The result does not yet meet the anti-retreat demand that no MODEL-tag step survive: the unconditional lift to arbitrary joint operators without pure-tensor factorization remains future work, and would either rederive factorization from a stricter substrate axiom or drop it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.