Local B Readout Residual Dimension

Abstract

Local B readout leaves the A-local and correlation sectors invisible.

Theorem 1.1 (The B-local invisible sector has the stated dimension).

$$\begin{array}{c}\forall m:\mathrm{Nat},n:\mathrm{Nat},m\ge 1\wedge n\ge 1\Rightarrow \\ \mathrm{finrankR}(\mathrm{bipartiteTraceZero}(m,n))={m\times n}^2-1\wedge \\ \mathrm{finrankR}(\mathrm{localBSector}(m,n))=n^2-1\wedge \\ \mathrm{finrankR}(\mathrm{Sup}(\mathrm{localASector}(m,n),\mathrm{correlationSector}(m,n)))=n^2\times m^2-1.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/LocalBReadoutResidualDimension.local_b_readout_residual_dimension (✓ std3). ∎

Source. Repository-derived.

Commentary.

The canonical bipartite traceless Hermitian carrier splits into the A-local, B-local, and correlation sectors.

A complete readout restricted to subsystem B occupies the B-local sector. Its invisible complement is the orthogonal join of the A-local and correlation sectors.

The imported sector decomposition supplies orthogonality and the individual ranks; finite-dimensional join formulas give all three displayed dimensions.

References

• Truth anchor: D5/S3/Quantum/Entanglement/LocalBReadoutResidualDimension.local_b_readout_residual_dimension
• Dependency: D5/S3/Quantum/Entanglement/BipartiteSectorDecomposition