Paired Complex-Channel Dimension Capacity
Abstract
Paired complex channels have two complex dimensions of capacity per finite sensor.
Definition 1.1 (Paired-channel capacity).
Lean statement: D5/S3/Weil/Pick/PairedComplexChannelDimensionCapacity.pairedComplexChannelCapacity
Formalization. D5/S3/Weil/Pick/PairedComplexChannelDimensionCapacity.pairedComplexChannelCapacity (✓ std3).
Source. Repository-derived.
Commentary.
The capacity is the finite sensor cardinality multiplied by two, one complex coordinate for each member of the reflected channel pair.
Theorem 1.2 (Dimension excess forces a blind direction).
Proof. Machine-checked in Lean as D5/S3/Weil/Pick/PairedComplexChannelDimensionCapacity.paired_complex_channel_dimension_capacity (✓ std3). ∎
Source. Repository-derived.
Commentary.
Injectivity into the paired observation codomain bounds the source finrank by the channel capacity. Rank-nullity also gives a quantitative lower bound on the blind-space dimension.
When the source finrank strictly exceeds capacity, noninjectivity produces two distinct states with the same reading. Their difference is an explicit nonzero vector annihilated by every paired channel.