Finite Informational Effect Certificate

Abstract

Informationally complete quantum effects admit a dimension-bounded finite certificate.

Theorem 1.1 (A finite effect subfamily retains informational completeness).

$$\begin{gathered} \forall d:\mathrm{Nat},\mathrm{NeZero}(d), \\ I:\mathrm{Type}, \\ E:I\to \{A:\mathrm{HermitianSpace}(d)\mid \mathrm{PosSemidef}(\mathrm{matrix}(A))\wedge \mathrm{PosSemidef}(1-\mathrm{matrix}(A))\}, \\ \mathrm{Injective}((\rho :\mathrm{DensityState}(\mathrm{Fin}(d))\mapsto (i:I\mapsto \Re \mathrm{Tr}(\mathrm{matrix}(\rho )\mathrm{matrix}(E(i))))))\Rightarrow \\ \exists S:\mathrm{Finset}(I),\mathrm{card}(S)\le d^2-1\wedge \\ \mathrm{span}(\mathbb{R},\{\mathrm{centeredHermitianMap}(d,E(i)):i\in S\})=\mathrm{traceZeroHermitian}(d)\wedge \\ \mathrm{Injective}((\rho :\mathrm{DensityState}(\mathrm{Fin}(d))\mapsto (i\in S\mapsto \Re \mathrm{Tr}(\mathrm{matrix}(\rho )\mathrm{matrix}(E(i)))))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/PredictionDepth/FiniteInformationalEffectCertificate.finite_informational_effect_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source family consists of positive Hermitian effects bounded above by the identity. Its trace readout is injective on the canonical positive trace-one density states.

Canonical trace removal turns informational completeness into full span of the real trace-zero Hermitian carrier. Finite-dimensional basis extraction chooses source indices rather than replacement vectors, so the selected original effects still separate states.

References

• Truth anchor: D5/S3/Quantum/PredictionDepth/FiniteInformationalEffectCertificate.finite_informational_effect_certificate
• Dependency: D5/S3/Quantum/PredictionDepth/FiniteSequentialWordCertificate
• Dependency: D5/S3/Quantum/Tomography/InformationalCompletenessEquivalence