IndisputableMonolith.Gravity.QuantumChannel.SubstrateSemanticsUnconditional
Every complex-linear map on the eight-tick signal space arises as the induced channel of a joint substrate operator under a fixed canonical probe. The witness is the product operator id tensor L, which recovers L exactly. Gravity Track 2.C cites this to retire residual semantic hypotheses and equate amplitude-linearity with substrate access. The argument is structural: construct the operator, check the induced channel, then close the density-only obstruction.
claimFor every $\mathbb{C}$-linear map $L:\mathrm{Signal}_8\to\mathrm{Signal}_8$, the joint operator $\mathrm{id}\otimes L$ on the substrate, under the canonical recognition probe $(\psi_0=1,\,i_0=0,\,\chi=1)$, has induced channel equal to $L$. Consequently amplitude-linearity is equivalent to arising from substrate access, and no nontrivial amplitude-linear channel is density-only.
background
Gravity Track 2.C treats quantum channels on the eight-tick signal space as the interface between recognition probes and the joint substrate. Upstream, Substrate Locality / Measurement-Access Principle (structural theorem, zero sorry) fixes how a local access map extracts an induced channel from a joint linear operator.
This module supplies the universal witness: given any $\mathbb{C}$-linear $L$ on $\mathrm{Signal}_8$, form $\mathrm{id}\otimes L$. Under the canonical probe $(\psi_0=1, i_0=0, \chi=1)$, the induced channel is exactly $L$. Amplitude-linearity is the structural property that a channel behaves linearly on amplitudes rather than only on densities.
The local setting is unconditional substrate semantics: every amplitude-linear channel is realized by some joint substrate operator, with no residual RS-internal axiom. Sibling certificates package the equivalence and the density-only vanishing statement into a single inhabited certificate.
proof idea
Construct the universal substrate-access operator as $\mathrm{id}\otimes L$ and the canonical access triple. Verify that the induced channel of this operator equals $L$ by the access calculus from SubstrateLocalAccess.
From that identity, every amplitude-linear channel arises from substrate access; the converse direction is the access definition, yielding the iff. Density-only amplitude-linear channels are forced to zero by the same identity, so no nontrivial example exists. A thin certificate record and an inhabited instance bundle the statements for downstream import.
why it matters in Recognition Science
Downstream, PhysicalChannelAmplitudeLinear imports this module as the unconditional closure of Track 2.C: the retirement chain through Sessions 85-126 converges on amplitude-linearity as the only surviving channel class, now grounded in substrate access rather than a semantic hypothesis.
In the Recognition framework this sits on the gravity quantum-channel side of the forcing story. It does not re-prove T0-T8, but it makes the channel interface compatible with the eight-tick octave (T7) and with substrate locality already closed upstream. Parent modules can quote the certificate or the one-statement theorem instead of re-opening access constructions.
The density-only obstruction is the practical payoff: channels that ignore amplitude structure cannot carry nontrivial recognition dynamics once substrate semantics is unconditional.
scope and limits
- Does not derive amplitude-linearity from T0-T8; it only supplies substrate semantics for that class.
- Does not construct physical Hamiltonians or mass-ladder data; the objects are linear maps on Signal8.
- Does not claim uniqueness of the joint operator beyond the universal id tensor L witness.
- Does not address nonlinear or non-complex-linear channels.
- Does not reopen SubstrateLocalAccess; it consumes that module as given.
used by (1)
depends on (1)
declarations in this module (11)
-
def
universalSubstrateAccessOperator -
def
canonicalAccess -
theorem
universalSubstrateAccessOperator_inducedChannel -
theorem
arisesFromSubstrateAccess_of_isAmplitudeLinear -
theorem
isAmplitudeLinear_iff_arisesFromSubstrateAccess -
theorem
channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional -
theorem
not_exists_nontrivial_isAmplitudeLinear_isDensityOnly_unconditional -
structure
SubstrateSemanticsUnconditionalCert -
def
substrateSemanticsUnconditionalCert -
theorem
substrateSemanticsUnconditionalCert_inhabited -
theorem
unconditional_substrate_semantics_one_statement