Single-Prime Visible Space

Abstract

Single-prime Hermitian effects see exactly the scalar and singleton sectors.

Theorem 1.1 (Single-prime readout leaves exactly the cross-prime sectors invisible).

$$\begin{array}{c}\forall \iota :\mathrm{Type}(),\mathrm{Fintype}(\iota ),\mathrm{DecidableEq}(\iota ),\\ d:\iota \to \mathrm{Nat}(),\\ \mathrm{IsInternal}(S\mapsto \mathrm{primeSector}(d,S))\wedge \\ (\forall S:\mathrm{Finset}(\iota ),\mathrm{finrankR}(\mathrm{primeSector}(d,S))=\prod _{j\in S}d{\left(j\right)}^2-1)\Rightarrow \\ \mathrm{singlePrimeVisibleSpace}(d)=\mathrm{Sup}(\mathrm{primeSector}(d,\varnothing ),\mathrm{iSup}(i,i\mapsto \mathrm{primeSector}(d,\{i\})))\wedge \\ \mathrm{finrankR}(\mathrm{singlePrimeVisibleSpace}(d))=1+\sum _{i\in \iota }d{\left(i\right)}^2-1\wedge \\ \mathrm{finrankR}(\mathrm{invisibleTraceZeroResidual}(d))={\prod _{i\in \iota }d\left(i\right)}^2-1-\sum _{i\in \iota }d{\left(i\right)}^2-1\wedge \\ \mathrm{invisibleTraceZeroResidual}(d)=\mathrm{iSup}(\{S:\mathrm{Finset}(\iota )\mid 2\le \mathrm{card}(S)\},S\mapsto \mathrm{primeSector}(d,S)).\end{array}$$

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

Source. Repository-derived.

Commentary.

For a finite family of local Hilbert dimensions, primeSector is the repository’s canonical tensor sector: factors in S are traceless Hermitian and factors outside S are scalar Hermitian.

The standing internal-decomposition and sector-rank hypotheses are the formal counterparts of the orthogonal sector expansion immediately preceding theorem 119.1 in the source.

The four conclusion clauses identify the visible space, compute its real dimension, compute the invisible trace-zero residual dimension, and identify that residual with exactly the sectors supported on at least two factors.

References

• Truth anchor: D5/S3/Quantum/Entanglement/SinglePrimeVisibleSpace.single_prime_visible_space
• Dependency: D5/S3/Quantum/Dynamics/ProductDynamicsLocalSupport
• Dependency: D5/S3/Quantum/Entanglement/BipartiteSectorDecomposition