IncoherentCone

Abstract

Finite-dimensional spectral and overlap bounds for antidistinguishability.

Theorem 1.1 (psd closed).

$$\forall (n:\mathbb{N}),\mathrm{IsClosed}\{A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}|(A).\mathrm{PosSemidef}\}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/IncoherentCone.psd_closed (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The positive semidefinite matrices form a closed set.

Theorem 1.2 (flatten inner).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),\forall (Z:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),\mathrm{inner}\mathbb{R}(D5.S3.\mathrm{Quantum}.\mathrm{Matrix}.\mathrm{CartesianVariance}.\mathrm{vectorize}nA)(D5.S3.\mathrm{Quantum}.\mathrm{Matrix}.\mathrm{CartesianVariance}.\mathrm{vectorize}nZ)=\mathrm{RHLinalg}.\mathrm{rtrace}((A).\mathrm{conjTranspose}\cdot Z)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/IncoherentCone.flatten_inner (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The real inner product after vectorization equals the real trace pairing.

Theorem 1.3 (trace hermitianPart).

$$\forall (n:\mathbb{N}),\forall (G:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),((G).\mathrm{IsHermitian})\to \forall (Z:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),\mathrm{RHLinalg}.\mathrm{rtrace}(G\cdot (\mathrm{selfAdjointPart}\mathbb{R}Z:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}))=\mathrm{RHLinalg}.\mathrm{rtrace}(G\cdot Z)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/IncoherentCone.trace_hermitianPart (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The trace pairing with a Hermitian matrix depends only on the self-adjoint part of the other matrix.

Theorem 1.4 (rankone trace).

$$\forall (n:\mathbb{N}),\forall (Y:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),\forall (x:\mathrm{Fin}n\to \mathbb{C}),\mathrm{RHLinalg}.\mathrm{rtrace}(\mathrm{Matrix}.\mathrm{vecMulVec}(x)(\mathrm{star}(x))\cdot Y)=\mathrm{RHLinalg}.\mathrm{hermForm}Yx$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/IncoherentCone.rankone_trace (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The trace pairing with an outer product equals the Hermitian quadratic form.

Theorem 1.5 (psd entry bound of trace).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),((A).\mathrm{PosSemidef})\to \forall (R:\mathbb{R}),(0<R)\to (\mathrm{RHLinalg}.\mathrm{rtrace}(A)\le R)\to \forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Fin}n),\Vert Aij\Vert \le R$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/IncoherentCone.psd_entry_bound_of_trace (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

A positive semidefinite matrix with real trace at most a positive R has every entry of norm at most R.

Theorem 1.6 (incoherent closed).

$$\forall (n:\mathbb{N}),IsClosed\{A:Matrix(Finn)(Finn)\mathbb{C}|IsIncoherentA\}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/IncoherentCone.incoherent_closed (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The formula states the complete estimate or implication. Matrix entries, finite index sets, and proof parameters retain their Lean meanings. Proof fields of finite-index constructors are omitted.

Theorem 1.7 (incoherent separation).

$$\forall (n:\mathbb{N})(A:Matrix(Finn)(Finn)\mathbb{C}),(A.IsHermitian)\to (\neg IsIncoherentA)\to \exists Y:Matrix(Finn)(Finn)\mathbb{C},LocallyPsdY\wedge RHLinalg.rtrace(A\cdot Y)<0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/IncoherentCone.incoherent_separation (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston, Vincent Russo, Jamie Sikora (2025). Tight bounds for antidistinguishability and circulant sets of pure quantum states. DOI: 10.22331/q-2025-02-04-1622. URL: https://arxiv.org/abs/2311.17047v2.

Commentary.

The formula states the complete estimate or implication. Matrix entries, finite index sets, and proof parameters retain their Lean meanings. Proof fields of finite-index constructors are omitted.

References

• Truth anchor: D5/S3/Quantum/Measurement/IncoherentCone.flatten_inner
• Truth anchor: D5/S3/Quantum/Measurement/IncoherentCone.incoherent_closed
• Truth anchor: D5/S3/Quantum/Measurement/IncoherentCone.incoherent_separation
• Truth anchor: D5/S3/Quantum/Measurement/IncoherentCone.psd_closed
• Truth anchor: D5/S3/Quantum/Measurement/IncoherentCone.psd_entry_bound_of_trace
• Truth anchor: D5/S3/Quantum/Measurement/IncoherentCone.rankone_trace
• Truth anchor: D5/S3/Quantum/Measurement/IncoherentCone.trace_hermitianPart
• Dependency: D5/S3/Quantum/Matrix/CartesianVariance
• Dependency: D5/S3/Quantum/Measurement/AntidistinguishabilityGram