Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.PhysicalChannelAmplitudeLinear

show as:
view Lean formalization →

Under T0-T8 substrate semantics, physical channel response is the map from preparing a matter probe, applying C-linear joint dynamics, reading one channel coordinate, and calibrating. The module shows every such response is amplitude-linear, rules out nontrivial density-only responses, and certifies the canonical joint dynamics. Track 2.C and fork-handoff authors cite it. Proofs package upstream substrate-semantics and amplitude-linear forced-substrate results.

claimA map $R_C$ on eight-tick signals is a physical channel response of a $\mathbb{C}$-linear joint dynamics $R_J$ if there exist a matter probe $\psi_0$, channel index $i_0$, and nonzero scalar $\chi$ with $R_C\varphi = \chi^{-1}\cdot\mathrm{extract}_{i_0}(R_J(\mathrm{insert}(\psi_0,\varphi)))$. Any such $R_C$ is amplitude-linear; no nontrivial density-only physical channel response exists. For canonical T0-T8 joint dynamics, the recognition update is amplitude-linear and not density-only.

background

Gravity Track 2.C treats quantum channels on the eight-tick signal space as the observable shadow of joint dynamics on a matter-plus-channel substrate. The only substrate-internal measurement is: prepare a fixed matter probe, insert the channel signal, apply the joint map, extract one channel coordinate, and rescale by a calibration constant. Session 124 called this arising-from-substrate-access; this module renames it physical channel response so the operational meaning is explicit.

Upstream, SubstrateSemanticsUnconditional closes the substrate-access thread with no remaining RS-internal axioms, and AmplitudeLinearForcedSubstrate records the single-factor dichotomy: amplitude-linear and density-only forces the zero map (Sessions 85-86). Amplitude-linear means the channel acts linearly on complex amplitudes; density-only means it depends only on modulus-squared data. The local setting is the T0-T8 forcing chain (eight-tick octave, D = 3) specialized to joint substrate dynamics.

proof idea

The module is definition-first, then a short theorem stack. It introduces physical channel response as the substrate-access predicate (probe, index, nonzero calibration). Linear extension lemmas identify the induced channel with the unique C-linear extension of that response. Amplitude-linearity of any physical channel response is obtained by transporting the forced-substrate dichotomy through the access diagram. Density-only responses are shown to vanish, hence no nontrivial density-only physical channel response exists. A canonical T0-T8 joint-dynamics witness is built; its recognition update is proved amplitude-linear and not density-only. A certificate bundle packages these facts for handoff.

why it matters in Recognition Science

This is the named operational definition of physical channel response on the T0-T8 substrate, plus the amplitude-linear closure that Track 2.C needs before many-body lift. Downstream it is imported by MasterTheoremHandoffIntegration, the Track 7 fork-handoff receipt: Fork C is exactly the Track 2.C many-body / PiTensorProduct amplitude-linear lift. Without a substrate-semantic, calibrated notion of channel response and the proof that it cannot be density-only, that fork has nothing to hand off. The module sits after unconditional substrate-semantics closure and turns the Session 85-86 dichotomy into a gravity-facing certificate usable by the master theorem integration lane.

scope and limits

used by (1)

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 (27)