AntidistinguishabilitySpectrum

Abstract

Finite-dimensional spectral and overlap bounds for antidistinguishability.

Definition 1.1 (SpectralBalanced).

$\forall (n : N) {G : M a t r i x (F inn) (F inn) C} (h G : G . I sHer mi t ian), Sp ec t r a lB a l an ce d h G = \forall (j : F inn), R e a l . s q r t (h G . e i g e n v a l u es j) \leq \sum i \in u ni v . er a se j, R e a l . s q r t (h G . e i g e n v a l u es i)$

Formalization. D5/S3/Quantum/Measurement/AntidistinguishabilitySpectrum.SpectralBalanced (✓ 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 displayed predicate compares every eigenvalue square root against the sum over its complement. It organizes the spectral pairing proof.

Theorem 1.2 (spectral balanced pairing nonneg).

$\forall (n : N), (1 \leq n) \to \forall (G Y : M a t r i x (F inn) (F inn) C) (h G : G . P os S e mi d e f), (Sp ec t r a lB a l an ce d h G . i sHer mi t ian) \to (L oc a ll y P s d Y) \to R H L ina l g . r t r a ce (G \cdot Y) \geq 0$

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

Source. Repository-derived.

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.3 (spectral sufficient antidistinguishable).

$\forall (n d : N), (2 \leq n) \to \forall (ψ : F inn \to E u c l i d e an Sp a ce C (F in d)), (R e a l . s q r t ((f u nk : F inn \mapsto (g r am P s d ψ) . i sHer mi t ian . e i g e n v a l u es (((f in C o n g r (n = F in t y p e . c a r d (F inn))) . t r an s R H L ina l g . e i g Eq u i v) k)) ⟨ 0 ⟩) \leq \sum i \in u ni v . er a se (⟨ 0 ⟩ : F inn), R e a l . s q r t ((f u nk : F inn \mapsto (g r am P s d ψ) . i sHer mi t ian . e i g e n v a l u es (((f in C o n g r (n = F in t y p e . c a r d (F inn))) . t r an s R H L ina l g . e i g Eq u i v) k)) i)) \to I s A n t i d i s t in gu i s hab l e ψ$

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

Citation. 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.

Theorem 5.1, page 12: “Let n ≥ 2 be an integer and let G ∈ Pos(ℂⁿ) be the Gram matrix of a set S of n pure states, and let λ₀ ≥ λ₁ ≥ ⋯ ≥ λₙ₋₁ be the eigenvalues of G.” Its displayed square-root inequality implies antidistinguishability. The ordered values are read through the canonical finite eigenvalue equivalence. The displayed Lean implication also applies to unnormalized vectors; normalization is not used in this implication.

References

Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilitySpectrum.SpectralBalanced
Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilitySpectrum.spectral_balanced_pairing_nonneg
Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilitySpectrum.spectral_sufficient_antidistinguishable
Dependency: D5/S3/Quantum/Measurement/IncoherentCone
Dependency: D5/S3/Quantum/Measurement/LocallyPositiveSpectrum

Keyboard shortcuts

trureturing — Discovering truth

AntidistinguishabilitySpectrum

Abstract

References