Finite Prime-Time Rectangle Certificate

Abstract

A finite dimension-bounded quantum certificate extends to a finite rectangular window.

Theorem 1.1 (A complete effect family has a complete finite rectangle).

$$\begin{gathered} \forall d\in \mathbb{N},\mathrm{NeZero}\left(d\right), \\ E:\mathbb{N}\times \mathbb{N}\to \mathrm{HermitianTraceZero}\left(\mathrm{Fin}\left(d\right)\right), \\ \mathrm{span}\left(\mathbb{R},\mathrm{range}\left(E\right)\right)=\mathrm{top}\left(\right)\Rightarrow \\ \exists S:\mathrm{Finset}\left(\mathbb{N}\times \mathbb{N}\right),\mathrm{card}\left(S\right)\le d^2-1\wedge \\ \mathrm{span}\left(\mathbb{R},\mathrm{range}\left(\mathrm{restrict}\left(E,S\right)\right)\right)=\mathrm{top}\left(\right)\wedge \\ (\forall \rho ,\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),(\forall q\in S,\Re (\mathrm{Tr}\left(\mathrm{matrix}\left(\rho \right)E\left((\mathrm{fst}\left(q\right),\mathrm{snd}\left(q\right))\right)\right))=\Re (\mathrm{Tr}\left(\mathrm{matrix}\left(\sigma \right)E\left((\mathrm{fst}\left(q\right),\mathrm{snd}\left(q\right))\right)\right)))\Rightarrow \rho =\sigma )\wedge \\ \text{let }J:=\mathrm{image}\left(fst,S\right);T:=1+\sup \left(snd,S\right); \\ \forall \rho ,\sigma :\mathrm{DensityState}\left(\mathrm{Fin}\left(d\right)\right),(\forall p\in J,t\in \mathbb{N},t<T,\Re (\mathrm{Tr}\left(\mathrm{matrix}\left(\rho \right)E\left((p,t)\right)\right))=\Re (\mathrm{Tr}\left(\mathrm{matrix}\left(\sigma \right)E\left((p,t)\right)\right)))\Rightarrow \rho =\sigma . \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The input family consists of centered effects on the canonical real trace-zero Hermitian carrier. If its full real span is the carrier, at most d squared minus one concrete index-time pairs already span it and separate all density states.

From those pairs, J is constructed as their first-coordinate image and T as one plus the supremum of their second coordinates. Every selected pair lies in J times the times below T, so equality on the whole rectangle implies equality on the selected certificate.

The proof imports the frozen finite-pair certificate and adds only the canonical finite-rectangle construction required by the source.

References

• Truth anchor: D5/S3/Quantum/PredictionDepth/FinitePrimeTimeRectangleCertificate.finite_prime_time_rectangle_certificate
• Dependency: D5/S3/Quantum/PredictionDepth/FinitePrimeTimeCertificate