Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.SubstrateSemanticsUnconditional

show as:
view Lean formalization →

Every amplitude-linear channel on the eight-tick signal space arises from a joint substrate-access operator under the canonical recognition probe. The module builds the universal witness id ⊗ L, equates amplitude-linearity with substrate-access origin, and shows density-only amplitude-linear channels vanish unconditionally. Track 2.C gravity consumers cite it for the substrate-semantic half of the unconditional closure. Arguments reduce induced-channel identities and zero-channel uniqueness off the local-access layer.

claimFor every $\mathbb{C}$-linear map $L:\mathrm{Signal}_8\to\mathrm{Signal}_8$, the joint operator $\mathrm{id}\otimes L$ induces $L$ under the canonical recognition probe $(\psi_0=1,\,i_0=0,\,\chi=1)$. A channel is amplitude-linear if and only if it arises from substrate access; no nontrivial amplitude-linear density-only channel exists.

background

Gravity Track 2.C treats quantum channels on the eight-tick signal space $\mathrm{Signal}_8$ as the readout layer of a joint substrate. Upstream Substrate Local Access (structural theorem, zero sorry) fixes the measurement-access principle: a channel is realized by probing a joint linear operator with a recognition access triple $(\psi_0,i_0,\chi)$.

This module supplies the universal substrate-access operator. Given any $\mathbb{C}$-linear witness $L$, form $\mathrm{id}\otimes L$ on the joint space; under the canonical access $(\psi_0=1,i_0=0,\chi=1)$ the induced channel is exactly $L$. Amplitude-linearity is thereby given a substrate-semantic meaning: the channel is the probe-induced map of some joint linear operator.

A parallel density-only constraint is handled unconditionally. The same access calculus forces any channel that is both amplitude-linear and density-only to be the zero channel, so no nontrivial mixed witness survives.

proof idea

The module is theorem-bearing, not a pure definition dump. It defines the universal operator $\mathrm{id}\otimes L$ and the canonical access triple, then proves the induced-channel identity by direct evaluation against the local-access readout lemmas. From that identity it obtains one direction of the equivalence (every amplitude-linear channel arises from substrate access) by exhibiting the witness; the converse is the definition of the arises-from predicate. Density-only vanishing is a separate uniqueness argument: amplitude-linearity plus density-only forces the channel to zero, hence no nontrivial such pair exists. A certificate bundle and a one-statement packaging lemma collect the equivalences for downstream import.

why it matters in Recognition Science

This module is the substrate-semantic half of Track 2.C's unconditional closure. Downstream PhysicalChannelAmplitudeLinear imports it to finish the T0-T8 substrate-semantic amplitude-linearity theorem (zero sorry, zero RS-internal axiom, closure 2026-05-22), where IsAmplitudeLinear is identified as the only surviving channel class after the Session 85-126 retirement chain. The universal operator supplies the constructive witness that every amplitude-linear map is probe-induced, so later gravity-channel results can quote substrate access rather than an abstract linearity hypothesis. It sits after Substrate Local Access and before the physical-channel packaging that ties the story to the forcing chain landmarks (eight-tick octave, recognition probe).

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)