recognitionUpdate
plain-language theorem explainer
Names the single-factor substrate recognition update on the eight-tick register as the bare cyclic shift of the signal. Gravity Track 2.C cites it as the default matter-side dynamics when forcing channel responses to be amplitude-linear. The body is a one-line abbreviation of the spectral cyclic shift.
Claim. Write $\mathrm{RU}:\mathrm{Signal}_8\to\mathrm{Signal}_8$ for the one-tick substrate recognition update on a single eight-component complex signal, and set $\mathrm{RU}$ equal to the cyclic shift of the register (the unique $\mathbb{C}$-linear single-tick recognition evolution from the discrete Schrödinger derivation).
background
Track 2.C closes the substrate side of the amplitude-linearity forcing for gravity quantum channels. Sessions 85–86 gave a single-factor dichotomy (amplitude-linear and density-only implies the zero map) and a joint lift: if a joint operator is $\mathbb{C}$-linear, factorizes on pure tensors through matter and channel responses, and the matter response is nontrivial, then the channel response is amplitude-linear. Those results assumed factorization; this module instantiates the matter factor with the actual substrate dynamics.
Signal8 is the canonical eight-tick carrier $\mathrm{Fin},8\to\mathbb{C}$ forced by the T7 octave (period $2^3$) after $D=3$. The one-tick recognition evolution on that carrier is the spectral cyclic shift. Upstream, schrodinger_linear records that this shift is $\mathbb{C}$-linear on arbitrary superpositions, and the macroscopic ledger packages the same map as a linear map cyclicShiftLinear. The foundation recognition operator later composes projector-after-shift; here only the bare shift is needed as the single-factor substrate update.
proof idea
Definitional abbreviation only: the name is bound to Spectral.cyclic_shift (equivalently the ledger's local cyclic_shift). No tactics or lemmas are applied at this site. Downstream lemmas then inherit linearity from schrodinger_linear / cyclicShiftLinear and nontriviality from evaluating the shift on a basis vector.
why it matters
This is the concrete matter-side plug-in for Track 2.C. Sibling theorems use it to discharge the nontriviality hypothesis of the Session 86 joint lift (recognitionUpdate_nontrivial), force any pure-tensor channel factor to be amplitude-linear (isAmplitudeLinear_channel_of_recognitionUpdate), and obtain the density-only no-go (not_exists_density_only_channel_with_recognitionUpdate). The canonical cyclic joint operator is built on the same substrate map.
In the broader chain it aligns with T7's eight-tick octave and the operator-core bridge: the bare cyclic shift is the propagation that, on the quarter-turn core, coincides with the structured recognition update (projector-after-shift). Downstream foundation records (RecognitionOperator, OperatorCore_Forced, T7_T8_To_OperatorCore_Bridge) treat that shift as the forced one-tick dynamics on Signal8. Without naming this substrate default, the amplitude-linear forcing on the channel side remains conditional on an abstract matter response.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.