Visible State-Space Dimension

Abstract

The visible density-state range is compact and convex, with the expected affine dimension bound and complete-observer dimension.

Theorem 1.1 (The visible state space has the expected affine dimension).

$$\forall d\in \mathrm{Nat}\left(\right),V\in \mathrm{MatrixOperatorSystem}\left(\mathrm{Fin}\left(d\right)\right),\mathrm{NeZero}\left(d\right)\Rightarrow \left(\mathrm{IsCompact}\left(\mathrm{range}\left(\mathrm{visibleStateReadout}\left(d,V\right)\right)\right)\wedge \left(\mathrm{ConvexR}\left(\mathrm{range}\left(\mathrm{visibleStateReadout}\left(d,V\right)\right)\right)\wedge \left(\mathrm{finrankR}\left(\mathrm{direction}\left(\mathrm{affineSpanR}\left(\mathrm{range}\left(\mathrm{visibleStateReadout}\left(d,V\right)\right)\right)\right)\right)\le \mathrm{finrankR}\left(\mathrm{carrier}\left(V\right)\right)-1\wedge \left(\mathrm{Injective}\left(\mathrm{visibleStateReadout}\left(d,V\right)\right)\Rightarrow \mathrm{finrankR}\left(\mathrm{direction}\left(\mathrm{affineSpanR}\left(\mathrm{range}\left(\mathrm{visibleStateReadout}\left(d,V\right)\right)\right)\right)\right)=d^2-1\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/VisibleStateSpaceDimension.visible_state_space_compact_convex_dimension (✓ std3). ∎

Source. Repository-derived.

Commentary.

The visible state is the canonical trace-pairing readout of density matrices, restricted to the supplied Hermitian operator system.

Density matrices form a compact convex set. A local order-unit perturbation argument identifies the affine directions of their visible image with the readout image of traceless Hermitian directions.

Evaluation at the identity has codimension one and vanishes on those directions, proving the upper bound. Injectivity of the visible readout makes the centered map injective and preserves all d squared minus one traceless degrees of freedom.

Theorem 1.2 (The actual normalized density domain is compact and convex).

$$\forall d\in \mathrm{Nat}\left(\right),[\mathrm{NeZero}\left(d\right)],\mathrm{IsCompact}\left(\mathrm{setOf}\left(M\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathrm{Complex}\left(\right)\right)\mapsto \mathrm{PosSemidef}\left(M\right)\wedge \mathrm{trace}\left(M\right)=1\right)\right)\wedge \mathrm{Convex}\left(\mathrm{Real}\left(\right),\mathrm{setOf}\left(M\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathrm{Complex}\left(\right)\right)\mapsto \mathrm{PosSemidef}\left(M\right)\wedge \mathrm{trace}\left(M\right)=1\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/VisibleStateSpaceDimension.density_matrix_set_compact_convex (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every nonzero dimension this is the set of all complex positive semidefinite matrices of trace one. Singular states are included. The same original supplier is used by the visible-image dimension proof and by the centered physical conjugation-quotient geometry.

References

• Truth anchor: D5/S3/Quantum/Measurements/VisibleStateSpaceDimension.density_matrix_set_compact_convex
• Truth anchor: D5/S3/Quantum/Measurements/VisibleStateSpaceDimension.visible_state_space_compact_convex_dimension
• Dependency: D5/S3/Quantum/Entanglement/BipartiteSectorDecomposition
• Dependency: D5/S3/Quantum/Fibers/FutureStatisticsEquivalence
• Dependency: D5/S3/Quantum/Fibers/PhysicalFiber