Paired Complex-Channel Completeness

Abstract

Positive paired complex-channel energies have exactly the common channel kernel and are definite exactly under joint separation.

Theorem 1.1 (Positive paired channels preserve the common kernel).

$$\forall V:\mathrm{Type},[\mathrm{AddCommGroup}(V)],[\mathrm{Module}(\mathbb{C},V)],I:\mathrm{Type},[\mathrm{Fintype}(I)],m:I\to \mathrm{LinearMap}(V,\mathbb{C}),p:I\to \mathrm{LinearMap}(V,\mathbb{C}),w:I\to \mathbb{R},\forall i:I,0<w(i)\Rightarrow \{x\mid \mathrm{pairedComplexChannelEnergy}(m,p,w,x)=0\}=\{x\mid \forall i:I,m_i(x)=0\wedge p_i(x)=0\}\wedge (\forall x:V,x\ne 0\Rightarrow 0<\mathrm{pairedComplexChannelEnergy}(m,p,w,x))⟺\mathrm{Injective}(\mathrm{pairedComplexObservation}(m,p)).$$

Proof. Machine-checked in Lean as D5/S3/Weil/Pick/PairedComplexChannelCompleteness.paired_complex_channel_completeness (✓ std3). ∎

Source. Repository-derived.

Commentary.

The energy is the finite sum of positive sensor weights times the two complex readout norm squares. Therefore zero total energy forces both channels to vanish at every sensor.

The same kernel identity converts strict positivity on every nonzero state into injectivity of the paired observation map, and conversely. No finite-dimensional premise on the state space is required.

References

• Truth anchor: D5/S3/Weil/Pick/PairedComplexChannelCompleteness.paired_complex_channel_completeness