recognitionUpdate_nontrivial
plain-language theorem explainer
The substrate recognition update (cyclic shift on the eight-slot signal) is nontrivial: some signal and slot yield a nonzero value after the update. Track 2.C forcing and the T0–T8 density-only no-go both cite this witness to discharge the matter-side nontriviality hypothesis. Proof is an explicit existential: constant-1 signal at slot 0 reduces to 1 ≠ 0.
Claim. There exist a signal $\psi_0$ on the eight-tick octave and an index $i_0 \in \{0,\ldots,7\}$ such that the substrate recognition update (the cyclic shift) applied to $\psi_0$ is nonzero at slot $i_0$.
background
Track 2.C closes the substrate side of amplitude-linearity forcing for gravity quantum channels. Prior sessions gave a single-factor dichotomy (amplitude-linear and density-only implies the zero map) and a joint lift: if a $\mathbb{C}$-linear joint operator factorizes on pure tensors through matter and channel responses, and the matter response is nontrivial, then the channel response is amplitude-linear.
This module plugs in the actual substrate dynamics on the matter factor: the cyclic shift on Signal8, the unique $\mathbb{C}$-linear single-tick recognition update from the Schrödinger derivation (packaged via the macroscopic ledger). Signal8 is the eight-component complex signal on the eight-tick octave (forcing chain T7). The local abbrev for the recognition update is exactly that cyclic shift as a map on signals.
The joint-lift theorem needs a concrete nontriviality witness for the matter factor. This declaration supplies it for substrate-default dynamics.
proof idea
Explicit witness: take the constant-1 signal and slot index $0$. The cyclic shift sends slot $0$ to the value formerly at slot $1$, so the updated signal at $0$ equals $1 \in \mathbb{C}$. The goal reduces to $1 \neq 0$, discharged by the primitive unit-nonzero lemma. Term-mode refine builds the existential triple; a show aligns the unfolded evaluation with that inequality.
why it matters
Listed among the substantive theorems of Track 2.C substrate-side closure. It discharges the nontriviality hypothesis of the Session 86 joint lift when matter dynamics is the substrate cyclic shift.
Immediate parents: (1) the Track 2.C forcing theorem, which obtains the witness and concludes that any channel response participating in a $\mathbb{C}$-linear pure-tensor factorization with this matter update is amplitude-linear; (2) the canonical T0–T8 statement that the recognition update is not density-only as a physical channel response, again by obtaining the witness and invoking the single-factor dichotomy.
Framework landmarks: T7 eight-tick octave as the signal carrier; the recognition operator's projector-after-shift specialized here to bare cyclic shift on one factor. Together with the companion no-go and zero-channel corollaries, it makes substrate-side forcing unconditional inside the binary-tensor model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.