Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForced

show as:
view Lean formalization →

On the eight-tick complex signal space, no nontrivial channel response is both amplitude-linear and density-only. The module defines those response classes and proves their only common element is the zero map. Gravity Track 2.C cites this single-factor substrate dichotomy as the Session 85 closure. The argument routes amplitude-linearity through phase equivariance, then forces vanishing under the density-only constraint.

claimOn the eight-tick carrier $S_8:=\{0,\ldots,7\}\to\mathbb{C}$, any response that is amplitude-linear (homogeneous under complex scaling of the signal) and density-only (depends only on pointwise $|\psi|^2$) must be identically zero. Equivalently, no nontrivial map on $S_8$ is simultaneously amplitude-linear and density-only.

background

Recognition Science forces an eight-tick octave (T7) and a cyclic shift on the ledger state. Upstream, Complex Structure Forcing records that this shift cannot be diagonalized over $\mathbb{R}$, so complexification is algebraically forced: the analytic carrier is $\mathrm{Fin},8\to\mathbb{C}$ (Signal8).

This module works on that carrier. Amplitude-linearity means the channel response scales linearly with complex amplitudes. Density-only means the response sees only local intensities $|\psi|^2$, not phase. Phase equivariance is the intermediate property implied by amplitude-linearity: a global phase rotation of the signal rotates the response accordingly.

The setting is Gravity Track 2.C (quantum-channel and mediator constraints): classical or density-only mediators are incompatible with amplitude-linear response on the forced complex substrate.

proof idea

The module introduces predicates for amplitude-linearity, phase equivariance, and density-only response on maps out of Signal8. A short lemma shows amplitude-linearity implies phase equivariance. Combining amplitude-linearity with density-only forces the response to vanish identically. Corollaries restate the dichotomy: a nonzero amplitude-linear map cannot be density-only, and no nontrivial map satisfies both properties at once.

why it matters in Recognition Science

Session 85 of Gravity Track 2.C closes here as the single-factor substrate dichotomy on Signal8. The master certificate module aggregates this closure for the binary-tensor model. The joint-substrate module lifts the same no-go to matter-plus-channel modelled as a binary tensor product. MediatorUniversalityBoundary cites the vector-level result without re-proving it: a vector response on Signal8 cannot be amplitude-linear, density-only, and nonzero. Downstream of T7 and Complex Structure Forcing, the dichotomy blocks classical density-only mediators on the forced complex carrier.

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)