AntidistinguishabilityOverlapNonTight

Abstract

Finite-dimensional spectral and overlap bounds for antidistinguishability.

Theorem 1.1 (squared modulus lipschitz).

$$\forall (z:\mathbb{C}),\forall (w:\mathbb{C}),(\Vert z\Vert \le 1)\to (\Vert w\Vert \le 1)\to |(\Vert z\Vert {)}^2-(\Vert w\Vert {)}^2|\le 2\cdot \Vert z-w\Vert$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.squared_modulus_lipschitz (✓ 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.

Squared norms on the complex unit ball are Lipschitz with constant two.

Theorem 1.2 (norm square gram factor).

$$\forall (n:\mathbb{N}),\forall (r:\mathbb{N}),\forall (V:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}r)\mathbb{C}),\mathrm{Matrix}.\mathrm{map}(\mathrm{RHLinalg}.\mathrm{normSqMatrix}(V\cdot (V).\mathrm{conjTranspose}))(\mathrm{algebraMap}\mathbb{RC})=(\mathrm{fun}(i:\mathrm{Fin}n)\mapsto \mathrm{Function}.\mathrm{uncurry}(D5.S3.\mathrm{Quantum}.\mathrm{PureState}.\mathrm{PureStateHandshake}.\mathrm{rankOneDensity}(Vi)))\cdot ((\mathrm{fun}(i:\mathrm{Fin}n)\mapsto \mathrm{Function}.\mathrm{uncurry}(D5.S3.\mathrm{Quantum}.\mathrm{PureState}.\mathrm{PureStateHandshake}.\mathrm{rankOneDensity}(Vi)))).\mathrm{conjTranspose}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.norm_square_gram_factor (✓ 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 entrywise squared-modulus Gram matrix factors through the outer products of its rows.

Theorem 1.3 (norm square gram rank).

$$\forall (n:\mathbb{N}),\forall (r:\mathbb{N}),\forall (V:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}r)\mathbb{C}),(\mathrm{RHLinalg}.\mathrm{normSqMatrix}(V\cdot (V).\mathrm{conjTranspose})).\mathrm{rank}\le r\cdot r$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.norm_square_gram_rank (✓ 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 squared-modulus Gram matrix of r-dimensional rows has rank at most r squared.

Definition 1.4 (IsTight).

$$\forall (n:\mathbb{N}),IsTightn=\forall \epsilon :\mathbb{R},\epsilon >0\to \exists (d:\mathbb{N})(\psi :Finn\to EuclideanSpace\mathbb{C}(Find)),(\forall (i:Finn),\Vert \psi i\Vert =1)\wedge (\forall (ij:Finn),i\ne j\to \Vert inner\mathbb{C}(\psi i)(\psi j){\Vert }^2\le cSqn+\epsilon )\wedge \neg IsAntidistinguishable\psi$$

Formalization. D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.IsTight (✓ 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.

Section 6, page 17: “We still do not know whether or not Corollary 5.4 is tight when n ≥ 5.” The displayed tightness condition uses a squared-overlap margin. For n ≥ 10 the source cap is positive, so squaring reparametrizes its positive margin.

Definition 1.5 (claim).

$$claim=\forall n:\mathbb{N},10\le n\to \neg IsTightn$$

Formalization. D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.claim (✓ 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.

Section 6, page 17: “We still do not know whether or not Corollary 5.4 is tight when n ≥ 5.” The statement answers the question by proving non-tightness for every n ≥ 10; n = 5,…,9 remain open.

Theorem 1.6 (quantitative antidistinguishability).

$$\forall (n:\mathbb{N}),10\le n\to \forall (d:\mathbb{N})(\psi :Finn\to EuclideanSpace\mathbb{C}(Find)),(\forall (i:Finn),\Vert \psi i\Vert =1)\to (\forall (ij:Finn),i\ne j\to \Vert inner\mathbb{C}(\psi i)(\psi j){\Vert }^2\le cSqn+deltan)\to IsAntidistinguishable\psi$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.quantitative_antidistinguishability (✓ 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 (result).

$$\forall n:\mathbb{N},10\le n\to \neg IsTightn$$

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

Resolves. Problems/johnston-russo-sikora-2025-antidistinguishability-tightness (proved) by D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.result.

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/AntidistinguishabilityOverlapNonTight.IsTight
• Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.claim
• Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.norm_square_gram_factor
• Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.norm_square_gram_rank
• Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.quantitative_antidistinguishability
• Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.result
• Truth anchor: D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight.squared_modulus_lipschitz
• Dependency: D5/S3/Quantum/Matrix/CommutatorGap
• Dependency: D5/S3/Quantum/Measurement/AntidistinguishabilitySpectrum
• Dependency: D5/S3/Quantum/Measurement/OverlapLowRankDistance
• Dependency: D5/S3/Quantum/PureState/PureStateHandshake
• Dependency: D5/S3/Quantum/TensorNetworks/BridgeGraph/QuantumMaxFlowBound