Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSubstrate

show as:
view Lean formalization →

Defines the single-factor substrate recognition update on Signal8 as the cyclic shift, and records that it is amplitude-linear, nontrivial, and incompatible with any density-only channel response. Gravity Track 2.C cites this as the bare substrate before the joint matter-plus-channel lift. The module packages the recognition update, its linearity facts, and the canonical cyclic joint operator with pure-tensor factorization.

claimOn the single-site carrier $\mathrm{Signal}_8$, the recognition update is the cyclic shift $U:\mathrm{Signal}_8\to\mathrm{Signal}_8$. This $U$ is amplitude-linear and nontrivial. No density-only channel response can realize $U$ nontrivially. The canonical cyclic joint operator on the binary tensor product factors as a pure tensor under the stated factorization hypothesis.

background

Gravity Track 2 upgrades the macroscopic ledger Hilbert carrier and then forces amplitude-linearity of physical channel response. The single-site carrier is $\mathrm{Signal}_8$, the eight-tick octave register from the forcing chain (T7). The recognition update on that carrier is the cyclic shift from the Schrödinger derivation (spectral cyclic shift), written here as a plain map $\mathrm{Signal}_8\to\mathrm{Signal}_8$.

Upstream, MacroscopicLedger discharges Track 2.A: the recognition update extends canonically and $\mathbb{C}$-linearly from the single-site carrier. AmplitudeLinearForcedJoint lifts the Session-85 single-factor dichotomy (no nontrivial response is both amplitude-linear and density-only) to the joint matter-plus-channel substrate modelled as a binary tensor product.

This module sits between those layers: it names the bare substrate update, proves its amplitude-linearity and nontriviality, and introduces the canonical cyclic joint operator used by the joint lift.

proof idea

Definition-first module with short structural lemmas, not a long derivation. The recognition update is identified with the cyclic shift on $\mathrm{Signal}_8$. Amplitude-linearity and nontriviality are recorded directly from that identification. Density-only incompatibility is the single-factor dichotomy: if a channel response is density-only and matches the recognition update, it must be the zero channel; hence no nontrivial density-only channel carries the update. The canonical cyclic joint operator is defined on the binary tensor product, with a pure-tensor factorization lemma under the joint-model hypothesis used downstream.

why it matters in Recognition Science

Track 2.C needs an explicit substrate object before joint forcing and certification. This module supplies that object and the single-factor facts that Session 85 closed.

It is imported by AmplitudeLinearForcedCert (master certificate aggregating Sessions 85–87), by AmplitudeLinearForcedSectionReadout (section-readout forcing that retires full pure-tensor factorization), and by PhysicalChannelAmplitudeLinear (unconditional T0–T8 substrate-semantic amplitude-linearity closure). Downstream docs treat $\mathrm{IsAmplitudeLinear}$ as the only surviving semantic after the retirement chain; the substrate update and joint operator defined here are the concrete maps those certificates quantify over.

In the broader RS picture this is the eight-tick (T7) cyclic dynamics on the ledger carrier, not a new dynamical law.

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)