isAmplitudeLinear_recognitionUpdate
plain-language theorem explainer
The single-tick substrate recognition update on eight-slot signals is amplitude-linear over ℂ. Gravity and quantum-channel arguments that need the matter factor to be Schrödinger-linear cite this packaging. The proof is a two-field structure witness: the macroscopic cyclic-shift linearity lemma plus reflexivity of the equality to that linear map.
Claim. The substrate recognition update $R$ on eight-tick signals is amplitude-linear: there is a $\mathbb{C}$-linear map $L$ (the cyclic shift) such that $R=L$ as maps $\mathrm{Signal}_8\to\mathrm{Signal}_8$.
background
Track 2.C closes the substrate side of the amplitude-versus-density dichotomy for recognition channels. Sessions 85–86 already give a single-factor dichotomy (amplitude-linear and density-only forces the zero map) and a joint lift: a $\mathbb{C}$-linear joint operator that factorizes on pure tensors through a nontrivial matter response forces the channel factor to be amplitude-linear. Both were conditional on abstract factorization hypotheses.
This module plugs in the concrete matter dynamics: the unique $\mathbb{C}$-linear single-tick update on $\mathrm{Signal}_8$, the cyclic shift $T$ with $(Tf)(k)=f(k+1\bmod 8)$. That operator is the discrete time generator from complex-structure forcing and the Schrödinger derivation; MacroscopicLedger packages its linearity as cyclicShiftLinear. Amplitude-linearity here means the response acts linearly on complex amplitudes, not merely on densities $|\psi|^2$.
The eight-slot domain is the T7 octave (period $2^3$). The local recognitionUpdate is that cyclic-shift substrate dynamics on the single-factor side.
proof idea
Term-mode structure introduction. IsAmplitudeLinear recognitionUpdate is witnessed by the pair consisting of MacroscopicLedger's cyclicShiftLinear (the $\mathbb{C}$-linear cyclic shift on eight-tick signals) and the pointwise proof fun _ => rfl that the named recognition update agrees with that linear map. No further rewriting or case analysis.
why it matters
This is the single-factor packaging of Schrödinger linearity needed for Track 2.C substrate-side forcing. Downstream, isAmplitudeLinear_channel_of_recognitionUpdate lifts Session 86: any channel factor in a $\mathbb{C}$-linear pure-tensor joint operator with this matter update is forced amplitude-linear. Composing with Session 85 yields channel_eq_zero_of_density_only_of_recognitionUpdate and the existence no-go not_exists_density_only_channel_with_recognitionUpdate.
The parent physical no-go not_exists_nontrivial_density_only_physicalChannelResponse quotes the unconditional T0–T8 ban on nontrivial density-only physical channel responses; this lemma supplies the matter-side amplitude-linearity that makes the CPTP-classical mediator obstruction substrate-forced rather than hypothetical. Framework landmarks: T7 eight-tick octave as the signal domain, and the cyclic shift as the unique linear single-tick recognition update.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.