OverlapLowRankDistance

Abstract

Finite-dimensional spectral and overlap bounds for antidistinguishability.

Theorem 1.1 (A scalar lower bound for every eigenvalue).

$$\forall I:Type,[Fintype\left(I\right)][DecidableEq\left(I\right)],\forall A:Matrix\left(I,I,\mathbb{C}\right),\forall h:(A).IsHermitian,\forall a:\mathbb{R},(A-a\cdot (1:Matrix\left(I,I,\mathbb{C}\right))).PosSemidef⟹\forall i:I,a\le (h).eigenvalues\left(i\right)$$

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

For a Hermitian matrix A on an arbitrary finite index type, positive semidefiniteness of A minus a times the identity implies that every eigenvalue of A is at least a. Evaluate the quadratic form on a unit eigenvector. The index type may be empty, in which case the conclusion has no instances.

Theorem 1.2 (cSq nonneg).

$$\forall (n:\mathbb{N}),(2\le n)\to 0\le cSqn$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.cSq_nonneg (✓ 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.3 (delta budget).

$$\forall (n:\mathbb{N}),(10\le n)\to ((n:\mathbb{R})-3)\cdot ((n:\mathbb{R})\cdot ((n:\mathbb{R})-1))\cdot deltan=((n:\mathbb{R})-9)/16$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.delta_budget (✓ 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.4 (frobSq add le twice).

$$\forall (n:\mathbb{N})(AB:Matrix(Finn)(Finn)\mathbb{C}),RHLinalg.frobSq(A+B)\le 2\cdot RHLinalg.frobSqA+2\cdot RHLinalg.frobSqB$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.frobSq_add_le_twice (✓ 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.5 (delta pos).

$$\forall (n:\mathbb{N}),(10\le n)\to 0<deltan$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.delta_pos (✓ 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.6 (cSq lt half).

$$\forall (n:\mathbb{N}),(2\le n)\to cSqn<1/2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.cSq_lt_half (✓ 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 (offDiag card).

$$\forall (n:\mathbb{N}),(((univ:Finset(Finn)).offDiag)).card=n\cdot (n-1)$$

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

Definition 1.8 (equalOverlap).

$$\forall (n:\mathbb{N})(c:\mathbb{R}),equalOverlapnc=(1-c)\cdot (1:Matrix(Finn)(Finn)\mathbb{C})+c\cdot Matrix.of(Function.const(Finn)(Function.const(Finn)(1:\mathbb{C})))$$

Formalization. D5/S3/Quantum/Measurement/OverlapLowRankDistance.equalOverlap (✓ 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 definition. Matrix entries, finite index sets, and proof parameters retain their Lean meanings. Proof fields of finite-index constructors are omitted.

Theorem 1.9 (low rank distance lower).

$$\forall (\iota :Type)[Fintype\iota ][DecidableEq\iota ]\{AB:Matrix\iota \iota \mathbb{C}\}(hA:A.IsHermitian),(B.IsHermitian)\to \forall (a:\mathbb{R}),(0\le a)\to (\forall (i:\iota ),a\le hA.eigenvaluesi)\to \forall (r:\mathbb{N}),(B.rank\le r)\to ((Fintype.card\iota :\mathbb{R})-r)\cdot a^2\le RHLinalg.frobSq(A-B)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.low_rank_distance_lower (✓ 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.10 (delta overlap budget).

$$\forall (n:\mathbb{N}),(10\le n)\to (2\cdot ((n:\mathbb{R})\cdot ((n:\mathbb{R})-1))\cdot deltan{)}^2\le ((n:\mathbb{R})-9)/64$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.delta_overlap_budget (✓ 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.11 (quantitative rank contradiction).

$$\forall (n:\mathbb{N}),(10\le n)\to \forall (dist2:\mathbb{R}),(dist2\le 2\cdot (((n:\mathbb{R})-9)/16)+2\cdot (((n:\mathbb{R})-9)/64))\to (((n:\mathbb{R})-9)\cdot (1-cSqn{)}^2\le dist2)\to False$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.quantitative_rank_contradiction (✓ 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.12 (overlap excess identity).

$$\forall (n:\mathbb{N}),(2\le n)\to \forall (G:Matrix(Finn)(Finn)\mathbb{C}),(\forall (i:Finn),Gii=1)\to (\sum p\in ((univ:Finset(Finn)).offDiag),(\Vert Gp.1p.2{\Vert }^2-cSqn))=RHLinalg.frobSqG-(n:\mathbb{R}{)}^2/2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.overlap_excess_identity (✓ 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.13 (equalOverlap low rank distance).

$$\forall (nr:\mathbb{N})(c:\mathbb{R}),(0\le c)\to (c\le 1)\to \forall (B:Matrix(Finn)(Finn)\mathbb{C}),(B.IsHermitian)\to (B.rank\le r)\to ((n:\mathbb{R})-r)\cdot (1-c{)}^2\le RHLinalg.frobSq(equalOverlapnc-B)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.equalOverlap_low_rank_distance (✓ 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.14 (overlap target distance bound).

$$\forall (n:\mathbb{N}),(2\le n)\to \forall (G:Matrix(Finn)(Finn)\mathbb{C}),(\forall (i:Finn),Gii=1)\to \forall (e:\mathbb{R}),(0\le e)\to (\forall (ij:Finn),i\ne j\to \Vert Gij{\Vert }^2\le cSqn+e)\to (0\le RHLinalg.frobSqG-(n:\mathbb{R}{)}^2/2)\to RHLinalg.frobSq((RHLinalg.normSqMatrixG).map(algebraMap\mathbb{RC})-equalOverlapn(cSqn))\le (2\cdot ((n:\mathbb{R})\cdot ((n:\mathbb{R})-1))\cdot e{)}^2$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OverlapLowRankDistance.overlap_target_distance_bound (✓ 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/OverlapLowRankDistance.cSq_lt_half
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.cSq_nonneg
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.delta_budget
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.delta_overlap_budget
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.delta_pos
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.eigenvalue_lower_of_psd_sub_scalar
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.equalOverlap
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.equalOverlap_low_rank_distance
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.frobSq_add_le_twice
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.low_rank_distance_lower
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.offDiag_card
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.overlap_excess_identity
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.overlap_target_distance_bound
• Truth anchor: D5/S3/Quantum/Measurement/OverlapLowRankDistance.quantitative_rank_contradiction
• Dependency: D5/S3/Quantum/Matrix/CartesianVariance
• Dependency: D5/S3/Quantum/Measurement/AntidistinguishabilityGram