Multifactor Correlation Sector Decomposition

Abstract

Finite Hermitian tensor products split into subset-indexed correlation sectors.

Theorem 1.1 (Correlation order decomposes the global traceless carrier).

$$\begin{array}{c}\forall I:\mathrm{Type},\mathrm{Fintype}\left(I\right),\\ d:I\to \mathbb{N},(\forall i:I,d\left(i\right)\ge 1)\Rightarrow \\ \mathrm{InternalDirectSum}\left(\mathrm{correlationSector}\left(d\right)\right)\wedge \\ \mathrm{iSupNonempty}\left(\mathrm{correlationSector}\left(d\right)\right)=\mathrm{traceZeroGlobal}\left(d\right)\wedge \\ \mathrm{finrankR}\left(\mathrm{traceZeroGlobal}\left(d\right)\right)={\prod _{i\in I}d\left(i\right)}^2-1\wedge \\ (\forall S:\mathrm{Finset}\left(I\right),\mathrm{finrankR}\left(\mathrm{correlationSector}\left(d,S\right)\right)=\prod _{i\in S}d{\left(i\right)}^2-1)\wedge \\ (\forall k\in \mathbb{N},\mathrm{finrankR}\left(\mathrm{unobservedHighOrder}\left(d,k\right)\right)=\sum _{S:\mathrm{Finset}\left(I\right),\mathrm{card}\left(S\right)>k}\prod _{i\in S}d{\left(i\right)}^2-1).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/MultifactorCorrelationSectorDecomposition.multifactor_correlation_sector_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite family of positive local dimensions, split each real Hermitian space into its scalar identity line and trace-zero subspace. Distributing the tensor product over these local splittings produces one sector for every subset of factors.

The sectors form an internal direct sum. The nonempty sectors are exactly the global trace-zero carrier, and the sector indexed by S has dimension equal to the product of d_i squared minus one over the indices in S.

Consequently, readouts retaining sectors of order at most k leave a residual whose dimension is the sum of those products over subsets of cardinality greater than k. This dimension statement does not assert that a nonzero high-order component is entangled.

The source statement omitted positivity of the local dimensions. The formal theorem assumes every d_i is nonzero: in dimension zero the identity is zero, so the scalar identity sector is not one-dimensional and the stated formulas fail.

References

• Truth anchor: D5/S3/Quantum/MultifactorCorrelationSectorDecomposition.multifactor_correlation_sector_decomposition
• Dependency: D5/S3/Quantum/Entanglement/BipartiteSectorDecomposition