Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForced

show as:
view Lean formalization →

On the eight-tick complex signal carrier, no nontrivial channel response is both amplitude-linear and density-only. Gravity Track 2.C (Session 85) cites this single-factor substrate dichotomy as the vector-level no-go. Predicates for amplitude-linearity, phase equivariance, and density-only dependence reduce the joint condition to the zero map.

claimLet $S$ be the space of eight-tick analytic signals $\mathrm{Fin}\,8\to\mathbb{C}$. A response $R$ on $S$ that is amplitude-linear (homogeneous under complex scaling of the carrier) and density-only (depends only on pointwise $|S|^2$) must be identically zero. Equivalently, no nonzero $R$ is simultaneously amplitude-linear and density-only.

background

Recognition Science forces an eight-tick octave (T7): the ledger shift is a cyclic operator of period $2^3$. The foundation module on complex structure forcing shows that this shift cannot be diagonalized over $\mathbb{R}$, so the natural signal carrier is complex. This module works on that carrier, abbreviated as maps $\mathrm{Fin},8\to\mathbb{C}$ (the canonical eight-tick analytic signal).

Three response properties are isolated. Amplitude-linearity means the channel scales linearly with complex amplitude of the signal. Phase equivariance is the weaker covariance under global $U(1)$ phase. Density-only means the response sees only the pointwise intensity $|S|^2$, not the phase structure. The local setting is Gravity Track 2.C: constraints on quantum-channel mediators built on this substrate.

proof idea

The module is a short predicate-and-lemma stack, not a definition-only file. It introduces the eight-tick signal type and the three predicates (amplitude-linear, phase-equivariant, density-only). Amplitude-linearity is shown to imply phase equivariance. Combining amplitude-linearity with density-only forces the response to be the zero map. Contrapositives then yield: a nonzero amplitude-linear response cannot be density-only, and no nontrivial response satisfies both properties at once.

why it matters in Recognition Science

This is the Session 85 single-factor substrate dichotomy for Gravity Track 2.C. The master certificate module aggregates it as the statement that on the eight-tick signal, no nontrivial channel response is simultaneously amplitude-linear and density-only. The joint-substrate lift imports it and extends the same dichotomy to a binary tensor product of matter-plus-channel degrees of freedom. The mediator universality boundary treats this vector-level no-go as already proved here (with the classical-mediator companion), and does not re-prove it: a vector response cannot be amplitude-linear, density-only, and nonzero. In the broader forcing chain it sits on T7 (eight-tick carrier) and the forced complex structure of the shift.

scope and limits

used by (3)

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