Channel Fixed-Block Decomposition

Abstract

A record channel fixes exactly the full matrix blocks on its record classes.

Theorem 1.1 (Channel fixed-block decomposition).

$$\begin{array}{r}\forall d,e:\mathbb{N},Lambda:\mathrm{Type},[\mathrm{Fintype}(Lambda)],[\mathrm{DecidableEq}(Lambda)],\\ \forall record:\mathrm{Fin}(d)\to \mathrm{Fin}(e)\to \mathbb{C},classOf:\mathrm{Fin}(d)\to Lambda,\\ (\forall i,j:\mathrm{Fin}(d),\mathrm{recordGram}(record,i,j)=1⟺classOf\left(i\right)=classOf\left(j\right))\Rightarrow \\ (\forall \rho :\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{recordChannel}(record,\rho )=\rho ⟺\forall i,j:\mathrm{Fin}(d),classOf\left(i\right)\ne classOf\left(j\right)\Rightarrow \mathrm{entry}(\rho ,i,j)=0)\wedge \\ (\forall blocks:\prod _{alpha:Lambda}\mathrm{Matrix}(\left\{classOf\left(i\right)=alpha\mid i\in \mathrm{Fin}(d)\right\},\left\{classOf\left(i\right)=alpha\mid i\in \mathrm{Fin}(d)\right\},\mathbb{C}),alpha:Lambda,i,j:\left\{classOf\left(i\right)=alpha\mid i\in \mathrm{Fin}(d)\right\},\mathrm{entry}(\mathrm{classifiedBlockAlgEquiv}(classOf)\left(blocks\right),i,j)=\mathrm{entry}(blocks\left(alpha\right),i,j)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/FixedAlgebra/ChannelFixedBlockDecomposition.channel_fixed_block_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let d and e be natural dimensions and Lambda a finite decidable record-class type. The environment record is a complex amplitude table, and classOf assigns each address to its record class.

The public classification premise identifies Gram entry one exactly with equality of record classes. The channel and Gram matrix are the canonical primitives imported from the record family.

The class-supported algebra is defined directly by vanishing of entries between different classes. It is not defined as the range of the block map or as the channel fixed set.

The named classifiedBlockAlgEquiv first embeds one full matrix algebra per proof-relevant class fiber and then applies the canonical sigma-fiber reindexing. The second displayed clause pins this equivalence to the original within-class matrix entries.

References

• Truth anchor: D5/S3/Quantum/FixedAlgebra/ChannelFixedBlockDecomposition.channel_fixed_block_decomposition
• Dependency: D5/S3/Quantum/FixedAlgebra/RecordFixedAlgebraDecomposition
• Dependency: D5/S3/Quantum/FixedAlgebra/SingletonRecordClassicality