Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSubstrate

show as:
view Lean formalization →

Single-factor substrate layer for Gravity Track 2.C: the recognition update on one Signal8 factor is the eight-tick cyclic shift, shown amplitude-linear and nontrivial, and incompatible with any density-only channel response. Also packages the canonical cyclic joint operator on the binary tensor product. Track 2.C certificates and the unconditional amplitude-linearity closure import it. Proofs are direct transfers of cyclic-shift algebra plus the Session-85 dichotomy.

claimOn a single eight-tick carrier $\mathrm{Signal}_8$, the recognition update $U$ is the cyclic shift. Then $U$ is amplitude-linear and nontrivial; if a channel response realizes $U$ and is density-only, it is the zero channel; equivalently, no density-only channel implements $U$. The canonical cyclic joint operator on the matter-plus-channel binary tensor product admits a pure-tensor factorization under the module's standing hypotheses.

background

Gravity Track 2.C forces amplitude-linearity of physical channel response on the Recognition Science substrate. Session 85 closed the single-factor dichotomy on $\mathrm{Signal}_8$: no nontrivial channel response is both amplitude-linear and density-only. Amplitude-linear means the response scales with complex amplitudes; density-only means it depends only on occupation densities, erasing phase.

The eight-tick carrier $\mathrm{Signal}_8$ is the discrete Hilbert factor tied to the T7 octave (period $2^3$). Its recognition update is the spectral cyclic shift, written here as a map $U:\mathrm{Signal}_8\to\mathrm{Signal}_8$. Upstream MacroscopicLedger (Track 2.A) already shows that this update extends canonically and $\mathbb{C}$-linearly from the single-site carrier to the macroscopic ledger Hilbert space.

The joint-substrate companion models matter-plus-channel as a binary tensor product and lifts the dichotomy there. This module stays on the single-factor side and records the concrete $U$ that later joint and certificate modules quote.

proof idea

Definition layer first: recognitionUpdate is the cyclic shift on $\mathrm{Signal}_8$, re-exported as an ordinary function. Amplitude-linearity and nontriviality of $U$ are one-line transfers of the corresponding cyclic-shift lemmas from the spectral/Schrödinger derivation stack.

Channel-side results apply the Session-85 dichotomy: if a channel realizes $U$ and is density-only, it vanishes; hence no density-only channel carries the recognition update. The joint half introduces the canonical cyclic joint operator on the binary tensor product and records its pure-tensor factorization identity, feeding later section-readout and certificate modules that still mention that hypothesis before retiring it.

why it matters in Recognition Science

This is the substrate anchor for Track 2.C. Downstream AmplitudeLinearForcedCert aggregates Sessions 85–87 into the master binary-tensor certificate and imports this module for the single-factor recognition update and its dichotomy corollaries. AmplitudeLinearForcedSectionReadout attacks the remaining pure-tensor factorization gap and needs the canonical cyclic joint operator defined here. PhysicalChannelAmplitudeLinear is the unconditional T0–T8 closure: it converges on amplitude-linearity as the only surviving channel semantics, and quotes this substrate package as the concrete $U$ that density-only responses cannot match.

In the broader forcing chain, the eight-tick cyclic shift is the T7 octave dynamics on the discrete carrier; pinning channel response to that update (and ruling out density-only realizations) is how Track 2.C turns ledger kinematics into a semantic constraint on gravity’s quantum channel.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)