canonicalRecognitionCoupled
plain-language theorem explainer
Canonical witness that the binary-tensor joint substrate is recognition-coupled: both matter and channel factors are the cyclic-shift recognition update, with joint operator their pure-tensor product map. Track 2.C structural theorems cite this as the concrete inhabitant of the recognition-coupled factorization hypothesis. Construction is a one-line extension of the canonical factorization; the coupling equality is reflexivity.
Claim. The canonical recognition-coupled factorization is the factorizable joint substrate on $\mathrm{Signal}_8 \otimes_{\mathbb{C}} \mathrm{Signal}_8$ whose matter response $R_M$ and channel response $R_C$ are both the substrate recognition update (cyclic shift), whose joint operator is $R_J = \mathrm{cyclic\_shift} \otimes \mathrm{cyclic\_shift}$, and which satisfies the coupling constraint $R_M = \mathrm{recognitionUpdate}$ by construction.
background
Track 2.C closes the gravitational-channel dichotomy on the binary-tensor model $\mathrm{Signal}8 \otimes{\mathbb{C}} \mathrm{Signal}_8$. Sessions 85–87 establish: no nontrivial single-factor response is both amplitude-linear and density-only; a $\mathbb{C}$-linear joint operator that factorizes on pure tensors forces each factor amplitude-linear under nontriviality of the other; and with the substrate recognition update on the matter side, the channel factor is forced amplitude-linear.
A factorizable joint substrate packages a joint operator $R_J$ together with factor responses $R_M$, $R_C$ and a pure-tensor factorization identity. Recognition-coupled factorization extends that package by the master-plan constraint $R_M = \mathrm{recognitionUpdate}$: matter dynamics is fixed by the T0–T8 forcing chain (single-site Schrödinger linearity forces the matter factor to be cyclic shift).
The upstream canonical factorization already sets both factors to the recognition update and $R_J$ to the tensor-product map of cyclic-shift linear maps. The present definition only packages that object under the recognition-coupled structure.
proof idea
Definitional construction, not a proof. The toFactorizableJointSubstrate field is set to the already-built canonical recognition factorization (both factors cyclic shift, joint operator the pure-tensor map). The remaining field matter_eq_recognitionUpdate is discharged by rfl, because that factorization already defines $R_M$ as recognitionUpdate. No lemmas are applied beyond the structure inheritance.
why it matters
This is the concrete witness that feeds every Track 2.C structural statement. Downstream, track2C_headline applied to it yields channel amplitude-linearity and density-only collapse to zero; those facts inhabit track2CCert, amplitude_linear_forced_canonical_prop, amplitudeLinearForcedStructuralCert, and the one-statement theorem amplitude_linear_forced_one_statement. The same witness also appears in the NoClassicalMediator substrate-inhabitation path.
In framework terms it upgrades paper IV's T2 from a MODEL tag to a STRUCTURAL THEOREM under the named factor-product axiom: the channel response is identified with the amplitude-linear extension as a substrate consequence, not a modeling choice. Matter dynamics is pinned by the T0–T8 chain (eight-tick octave, cyclic shift). The fully unconditional Track 2.C closure (retiring the factor-product hypothesis on general joint operators) remains open; this witness does not close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.