Target Prediction Sufficiency

Abstract

Visible targets are signature-determined; invisible targets separate physical states.

Theorem 1.1 (The visible span is exactly sufficient for target prediction).

$$\begin{array}{c}\forall d\in \mathbb{N},\mathrm{NeZero}(d),Index:\mathrm{Type},\\ E:Index\to \{X:\mathrm{HermitianSpace}(d)\mid \mathrm{PosSemidef}(\mathrm{matrix}(X))\wedge \mathrm{PosSemidef}(I-\mathrm{matrix}(X))\},\\ T:\mathrm{Submodule}(\mathbb{R},\mathrm{HermitianSpace}(d)),\\ \mathrm{let}V:\mathrm{Submodule}(\mathbb{R},\mathrm{HermitianSpace}(d))=\mathrm{span}(\mathbb{R},\mathrm{insert}(\mathrm{identityHermitian}(d),\mathrm{range}(E)))\\ [T\subseteq V\Rightarrow \forall A:\mathrm{HermitianSpace}(d),A\in T,\rho ,\sigma :\mathrm{DensityState}(\mathrm{Fin}(d)),(\forall i:Index,\mathrm{Tr}(\mathrm{matrix}(\rho )E\left(i\right))=\mathrm{Tr}(\mathrm{matrix}(\sigma )E\left(i\right)))\Rightarrow \mathrm{Tr}(\mathrm{matrix}(\rho )A)=\mathrm{Tr}(\mathrm{matrix}(\sigma )A)]\wedge \\ [\forall A:\mathrm{HermitianSpace}(d),\neg A\in V\Rightarrow \\ \exists D:\mathrm{HermitianSpace}(d),eps:\mathbb{R},rhoPlus,rhoMinus:\mathrm{DensityState}(\mathrm{Fin}(d)),\\ \mathrm{Tr}(D)=0\wedge D\in V^{\perp }\wedge \\ \mathrm{Tr}(DA)\ne 0\wedge 0<eps\wedge \\ \mathrm{matrix}(rhoPlus)=d^{-1}I+epsD\wedge \\ \mathrm{matrix}(rhoMinus)=d^{-1}I-epsD\wedge \\ (\forall i:Index,\mathrm{Tr}(\mathrm{matrix}(rhoPlus)E\left(i\right))=\mathrm{Tr}(\mathrm{matrix}(rhoMinus)E\left(i\right)))\wedge \\ \mathrm{Tr}(\mathrm{matrix}(rhoPlus)A)\ne \mathrm{Tr}(\mathrm{matrix}(rhoMinus)A)].\end{array}$$

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

Source. Repository-derived.

Commentary.

The visible real Hermitian subspace is constructed from the identity and the complete family of declared effects. If the target subspace lies inside it, equal physical-state signatures force equal expectations for every target observable.

For an observable outside the visible span, subtract its orthogonal projection. The resulting nonzero residual is trace zero and has a nonzero trace pairing with the observable.

Small symmetric perturbations of the maximally mixed state along that residual are density states. They agree on every current effect but have different expectation for the chosen observable.

References

• Truth anchor: D5/S3/Quantum/PredictionDepth/TargetPredictionSufficiency.target_prediction_sufficiency
• Dependency: D5/S3/Quantum/Measurement/IncompleteBudgetPhysicalCertificate