DetectorSensorDickeOptimality

Abstract

Balanced Dicke states maximize the success of equal-prior detector-sensor identification.

Theorem 1.1 (psd_cauchy_schwarz).

$$\forall (h:Type),[Fintype\left(h\right)],[DecidableEq\left(h\right)],(\forall (H:Matrix\left(h,h,\mathbb{C}\right)),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(H\right))\to (\forall (x:h\to \mathbb{C}),\forall (y:h\to \mathbb{C}),{\Vert dotProduct\left(star\left(x\right),\mathrm{Matrix}.\mathrm{mulVec}\left(H,y\right)\right)\Vert }^2\le \mathrm{Complex}.\mathrm{re}\left(dotProduct\left(star\left(x\right),\mathrm{Matrix}.\mathrm{mulVec}\left(H,x\right)\right)\right)\cdot \mathrm{Complex}.\mathrm{re}\left(dotProduct\left(star\left(y\right),\mathrm{Matrix}.\mathrm{mulVec}\left(H,y\right)\right)\right)))$$

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

Source. Repository-derived.

Commentary.

A positive semidefinite complex matrix satisfies Cauchy–Schwarz for its sesquilinear form: the squared absolute mixed value is bounded by the product of the two real diagonal values. The form may be degenerate.

Theorem 1.2 (P_sq).

$$\forall (n:\mathbb{N}),(0<n)\to ((\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{Inv}.\mathrm{inv}\left((\mathrm{Nat}.\mathrm{cast}\left(n\right):\mathbb{R})\right),\mathrm{Matrix}.\mathrm{of}\left(\mathrm{Function}.\mathrm{const}\left(Fin\left(n\right),\mathrm{Function}.\mathrm{const}\left(Fin\left(n\right),(1:\mathbb{C})\right)\right)\right)\right))\cdot (\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{Inv}.\mathrm{inv}\left((\mathrm{Nat}.\mathrm{cast}\left(n\right):\mathbb{R})\right),\mathrm{Matrix}.\mathrm{of}\left(\mathrm{Function}.\mathrm{const}\left(Fin\left(n\right),\mathrm{Function}.\mathrm{const}\left(Fin\left(n\right),(1:\mathbb{C})\right)\right)\right)\right))=\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{Inv}.\mathrm{inv}\left((\mathrm{Nat}.\mathrm{cast}\left(n\right):\mathbb{R})\right),\mathrm{Matrix}.\mathrm{of}\left(\mathrm{Function}.\mathrm{const}\left(Fin\left(n\right),\mathrm{Function}.\mathrm{const}\left(Fin\left(n\right),(1:\mathbb{C})\right)\right)\right)\right))$$

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

Source. Repository-derived.

Commentary.

The all-ones matrix divided by its positive dimension is idempotent.

Definition 1.3 (fire).

$$\forall (n:\mathbb{N}),\forall (theta:\mathbb{R}),\forall (i:Fin\left(n\right)),\forall (psi:\left(Fin\left(n\right)\to Bool\right)\to \mathbb{C}),fire\left(theta,i,psi\right)=(funx:Fin\left(n\right)\to Bool\mapsto \mathrm{Complex}.\exp \left((ifx\left(i\right)then1else-1)\cdot (theta:\mathbb{C})\cdot \mathrm{Complex}.I\right)\cdot psi\left(x\right))$$

Formalization. D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.fire (✓ std3).

Citation. C. Zhan, H. Gupta, M. Hillery (2024). Optimizing Initial State of Detector Sensors in Quantum Sensor Networks. DOI: 10.1145/3655028. URL: https://arxiv.org/abs/2306.17401v6.

Commentary.

Section 2, pages 2–3: “Let |𝜙ᵢ⟩ = (𝐼^{⊗𝑖} ⊗ 𝑈 ⊗ 𝐼^{⊗(𝑛−𝑖−1)})|𝜓⟩.” A Boolean word labels the tensor eigenbasis; true is u₊ and false is u₋. Angles are in radians.

Definition 1.4 (isoSuccess).

$$\forall (n:\mathbb{N}),\forall (theta:\mathbb{R}),\forall (psi:\left(Fin\left(n\right)\to Bool\right)\to \mathbb{C}),\forall (M:LocalPOVM\left(Fin\left(n\right)\to Bool,Fin\left(n\right)\right)),isoSuccess\left(theta,psi,M\right)=(1)/((n:\mathbb{R}))\cdot \sum i:Fin\left(n\right),\mathrm{Complex}.\mathrm{re}\left((star\left(fire\left(theta,i,psi\right)\right){\cdot }_v(\mathrm{LocalPOVM}.\mathrm{effect}\left(M,i\right){\times }_{v}fire\left(theta,i,psi\right)))\right)$$

Formalization. D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.isoSuccess (✓ std3).

Citation. C. Zhan, H. Gupta, M. Hillery (2024). Optimizing Initial State of Detector Sensors in Quantum Sensor Networks. DOI: 10.1145/3655028. URL: https://arxiv.org/abs/2306.17401v6.

Commentary.

Section 2, page 3: “these final states have an equal prior probability”. The success is the mean of the Born probabilities for the correct outcomes. LocalPOVM is the existing finite family of positive semidefinite effects summing to the identity.

Definition 1.5 (rCount).

$$\forall (n:\mathbb{N}),\forall (i:Fin\left(n\right)),\forall (j:Fin\left(n\right)),\forall (k:\mathbb{N}),rCount\left(n,i,j,k\right)=\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((funx:Fin\left(n\right)\to Bool\mapsto ((\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((funj:Fin\left(n\right)\mapsto x\left(j\right)=true),(\mathrm{Finset}.\mathrm{univ}:Finset\left(Fin\left(n\right)\right))\right)\right)=k)\wedge (x\left(i\right)=x\left(j\right)))),(\mathrm{Finset}.\mathrm{univ}:Finset\left(Fin\left(n\right)\to Bool\right))\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.rCount (✓ std3).

Citation. C. Zhan, H. Gupta, M. Hillery (2024). Optimizing Initial State of Detector Sensors in Quantum Sensor Networks. DOI: 10.1145/3655028. URL: https://arxiv.org/abs/2306.17401v6.

Commentary.

Section 4, page 7: “For each 0 ≤ 𝑘 ≤ 𝑛, let 𝑅𝑘 be the number of coefficient-squares from 𝑆𝑘 in the RHS of a Real equation”. Observation 1 places a word on this side exactly when its two selected bits agree. The inner cardinality counts the true bits.

Definition 1.6 (lCount).

$$\forall (n:\mathbb{N}),\forall (i:Fin\left(n\right)),\forall (j:Fin\left(n\right)),\forall (k:\mathbb{N}),lCount\left(n,i,j,k\right)=\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((funx:Fin\left(n\right)\to Bool\mapsto ((\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((funj:Fin\left(n\right)\mapsto x\left(j\right)=true),(\mathrm{Finset}.\mathrm{univ}:Finset\left(Fin\left(n\right)\right))\right)\right)=k)\wedge (x\left(i\right)\ne x\left(j\right)))),(\mathrm{Finset}.\mathrm{univ}:Finset\left(Fin\left(n\right)\to Bool\right))\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.lCount (✓ std3).

Citation. C. Zhan, H. Gupta, M. Hillery (2024). Optimizing Initial State of Detector Sensors in Quantum Sensor Networks. DOI: 10.1145/3655028. URL: https://arxiv.org/abs/2306.17401v6.

Commentary.

Section 4, page 7: “𝐿𝑘 be the number of coefficient-squares from 𝑆𝑙 in the LHS of Real equation.” Observation 1 places a word on this side exactly when its two selected bits differ. The source’s Sl in this sentence denotes the selected weight partition.

Definition 1.7 (T).

$$\forall (n:\mathbb{N}),T\left(n\right)=letq:\mathbb{N}=\mathrm{Nat}.\mathrm{div}\left((n+1),2\right)in(\mathrm{Real}.\arccos \left(-(((q:\mathbb{R})-1)/((q:\mathbb{R})))\right))/(2)$$

Formalization. D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.T (✓ std3).

Citation. C. Zhan, H. Gupta, M. Hillery (2024). Optimizing Initial State of Detector Sensors in Quantum Sensor Networks. DOI: 10.1145/3655028. URL: https://arxiv.org/abs/2306.17401v6.

Commentary.

Theorem 2, pages 6–7, defines T = ½ arccos(−(⌈n/2⌉ − 1)/⌈n/2⌉). Nat.div is integer division, so Nat.div (n + 1) 2 is the ceiling of n/2. The outer division is in ℝ.

Definition 1.8 (d).

$$\forall (n:\mathbb{N}),\forall (c:\mathbb{R}),d\left(n,c\right)=(\mathrm{Real}.\mathrm{sqrt}\left(1+((n:\mathbb{R})-1)\cdot c\right)+((n:\mathbb{R})-1)\cdot \mathrm{Real}.\mathrm{sqrt}\left(1-c\right))/((n:\mathbb{R}))$$

Formalization. D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.d (✓ std3).

Source. Repository-derived.

Commentary.

The real diagonal value of the square root of the constant-overlap Gram matrix.

Definition 1.9 (cstar).

$$\forall (n:\mathbb{N}),\forall (theta:\mathbb{R}),cstar\left(n,theta\right)=1-(4\cdot (\mathrm{Nat}.\mathrm{div}\left(n^2,4\right):\mathbb{R})\cdot \mathrm{Real}.\sin {\left(theta\right)}^2)/((n:\mathbb{R})\cdot ((n:\mathbb{R})-1))$$

Formalization. D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.cstar (✓ std3).

Source. Repository-derived.

Commentary.

The overlap determined by the maximal product of occupied and unoccupied sensor counts. The quotient n²/4 is taken in the natural numbers before coercion to the reals.

Theorem 1.10 (global_success_upper_bound).

$$\forall (n:\mathbb{N}),(3\le n)\to (\forall (theta:\mathbb{R}),(((0<theta)\wedge (theta\le T\left(n\right)))\vee ((\mathrm{Real}.\mathrm{pi}-T\left(n\right)\le theta)\wedge (theta<\mathrm{Real}.\mathrm{pi})))\to (\forall (psi:\left(Fin\left(n\right)\to Bool\right)\to \mathbb{C}),(\sum x:Fin\left(n\right)\to Bool,\mathrm{Complex}.\mathrm{normSq}\left(psi\left(x\right)\right)=1)\to (\forall (M:LocalPOVM\left(Fin\left(n\right)\to Bool,Fin\left(n\right)\right)),isoSuccess\left(theta,psi,M\right)\le d{\left(n,cstar\left(n,theta\right)\right)}^2)))$$

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

Source. Repository-derived.

Commentary.

Every normalized probe and every global POVM satisfy this success bound for at least three sensors in either admissible angle interval.

Definition 1.11 (claim).

$$claim=\forall (n:\mathbb{N}),(3\le n)\to (\forall (theta:\mathbb{R}),(((0<theta)\wedge (theta\le T\left(n\right)))\vee ((\mathrm{Real}.\mathrm{pi}-T\left(n\right)\le theta)\wedge (theta<\mathrm{Real}.\mathrm{pi})))\to (\forall (l:\mathbb{N}),(l\le n)\to ((IsMinOn\left((funk:\mathbb{N}\mapsto ((rCount\left(n,⟨0⟩,⟨1⟩,k\right):\mathbb{R})+\mathrm{Real}.\cos \left(2\cdot theta\right)\cdot (lCount\left(n,⟨0⟩,⟨1⟩,k\right):\mathbb{R}))/((rCount\left(n,⟨0⟩,⟨1⟩,k\right):\mathbb{R})+(lCount\left(n,⟨0⟩,⟨1⟩,k\right):\mathbb{R}))),\mathrm{Set}.\mathrm{Iic}\left(n\right),l\right))\to (\forall (phi:\left(Fin\left(n\right)\to Bool\right)\to \mathbb{C}),(\forall (x:Fin\left(n\right)\to Bool),\mathrm{Complex}.\mathrm{normSq}\left(phi\left(x\right)\right)=if\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((funj:Fin\left(n\right)\mapsto x\left(j\right)=true),(\mathrm{Finset}.\mathrm{univ}:Finset\left(Fin\left(n\right)\right))\right)\right)=lthen(1)/((\mathrm{Nat}.\mathrm{choose}\left(n,l\right):\mathbb{R}))else0)\to (\forall (psi:\left(Fin\left(n\right)\to Bool\right)\to \mathbb{C}),(\sum x:Fin\left(n\right)\to Bool,\mathrm{Complex}.\mathrm{normSq}\left(psi\left(x\right)\right)=1)\to (\forall (M:LocalPOVM\left(Fin\left(n\right)\to Bool,Fin\left(n\right)\right)),\exists (Mp:LocalPOVM\left(Fin\left(n\right)\to Bool,Fin\left(n\right)\right)),isoSuccess\left(theta,psi,M\right)\le isoSuccess\left(theta,phi,Mp\right)))))))$$

Formalization. D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.claim (✓ std3).

Citation. C. Zhan, H. Gupta, M. Hillery (2024). Optimizing Initial State of Detector Sensors in Quantum Sensor Networks. DOI: 10.1145/3655028. URL: https://arxiv.org/abs/2306.17401v6.

Commentary.

Section 5, Conjecture 1, page 10: “Consider the ISO problem, with the unitary operator 𝑈, initial state |𝜓⟩, and final states {|𝜙ᵢ⟩} as defined therein. Recall that the eigenvalues of 𝑈 are {𝑒^{+𝑖𝜃}, 𝑒^{−𝑖𝜃}}. Let 𝑛 ≥ 3 be the number of sensors. For a given 𝜃 ∈ (0,𝑇] ∪ [180 − 𝑇, 180), degrees, where 𝑇 is from Theorem 2, the optimal initial state |𝜓⟩ for the ISO problem is as follows. Let 𝑆ₗ be the partition that minimizes (𝑅ₗ + cos(2𝜃)𝐿ₗ)/(𝑅ₗ + 𝐿ₗ), where 𝑅ₗ and 𝐿ₗ are as defined in the previous section. The coefficients of the optimal solution are such that their coefficient-squares are given by: |𝜓ⱼ|² = 1/|𝑆ₗ| ∀ |𝜓ⱼ|² ∈ 𝑆ₗ |𝜓ⱼ|² = 0 ∀ |𝜓ⱼ|² ∉ 𝑆ₗ” The formula uses radians, φ for the proposed state and ψ for a competitor. Each minimizing l and every assignment of coefficient phases are allowed. The words of weight l number Nat.choose n l. The two Fin n indices have values 0 and 1; their proof fields are omitted.

Theorem 1.12 (weight_class_card).

$$\forall (n:\mathbb{N}),\forall (k:\mathbb{N}),\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((funx:Fin\left(n\right)\to Bool\mapsto \mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((funj:Fin\left(n\right)\mapsto x\left(j\right)=true),(\mathrm{Finset}.\mathrm{univ}:Finset\left(Fin\left(n\right)\right))\right)\right)=k),(\mathrm{Finset}.\mathrm{univ}:Finset\left(Fin\left(n\right)\to Bool\right))\right)\right)=\mathrm{Nat}.\mathrm{choose}\left(n,k\right)$$

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

Source. Repository-derived.

Acknowledgement. C. Zhan, H. Gupta, M. Hillery (2024). Optimizing Initial State of Detector Sensors in Quantum Sensor Networks. DOI: 10.1145/3655028. URL: https://arxiv.org/abs/2306.17401v6.

Commentary.

The Boolean words with exactly k true coordinates form a class of cardinality Nat.choose n k.

Theorem 1.13 (counts_partition).

$$\forall (n:\mathbb{N}),\forall (i:Fin\left(n\right)),\forall (j:Fin\left(n\right)),\forall (k:\mathbb{N}),rCount\left(n,i,j,k\right)+lCount\left(n,i,j,k\right)=\mathrm{Nat}.\mathrm{choose}\left(n,k\right)$$

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

Source. Repository-derived.

Commentary.

Agreement and disagreement of two selected bits partition each weight class.

Theorem 1.14 (pair_count_product).

$$\forall (n:\mathbb{N}),\forall (a:Fin\left(n\right)),\forall (b:Fin\left(n\right)),(a\ne b)\to (\forall (k:\mathbb{N}),lCount\left(n,a,b,k\right)\cdot (n\cdot (n-1))=2\cdot k\cdot (n-k)\cdot \mathrm{Nat}.\mathrm{choose}\left(n,k\right))$$

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

Source. Repository-derived.

Commentary.

For distinct sensor positions, counting disagreements over all ordered pairs gives twice the product of the occupied and unoccupied counts in each word.

Theorem 1.15 (dicke_normalized).

$$\forall (n:\mathbb{N}),\forall (l:\mathbb{N}),(l\le n)\to (\forall (phi:\left(Fin\left(n\right)\to Bool\right)\to \mathbb{C}),(\forall (x:Fin\left(n\right)\to Bool),\mathrm{Complex}.\mathrm{normSq}\left(phi\left(x\right)\right)=if\mathrm{Finset}.\mathrm{card}\left(\mathrm{Finset}.\mathrm{filter}\left((funj:Fin\left(n\right)\mapsto x\left(j\right)=true),(\mathrm{Finset}.\mathrm{univ}:Finset\left(Fin\left(n\right)\right))\right)\right)=lthen(1)/((\mathrm{Nat}.\mathrm{choose}\left(n,l\right):\mathbb{R}))else0)\to (\sum x:Fin\left(n\right)\to Bool,\mathrm{Complex}.\mathrm{normSq}\left(phi\left(x\right)\right)=1))$$

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

Source. Repository-derived.

Commentary.

A state with uniform squared amplitudes on a weight class has total squared norm one, independently of its coefficient phases.

Theorem 1.16 (result).

$$claim$$

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

Resolves. Problems/zhan-gupta-hillery-2024-detector-sensor-dicke-optimality (proved) by D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.result.

Source. Repository-derived.

Acknowledgement. C. Zhan, H. Gupta, M. Hillery (2024). Optimizing Initial State of Detector Sensors in Quantum Sensor Networks. DOI: 10.1145/3655028. URL: https://arxiv.org/abs/2306.17401v6.

Commentary.

Averaging a feasible Gram decomposition over sensor permutations preserves its objective and produces a real constant overlap. A positive semidefinite trace certificate bounds the objective by the squared diagonal of the Gram square root. This diagonal decreases with the overlap on the stated angle range. Every minimizing weight class reaches the smallest overlap, and a complete square-root measurement attains the bound. The argument allows arbitrary phases and every global POVM; it does not require the source’s stronger strict-averaging Conjecture 2.

References

• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.P_sq
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.T
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.claim
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.counts_partition
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.cstar
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.d
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.dicke_normalized
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.fire
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.global_success_upper_bound
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.isoSuccess
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.lCount
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.pair_count_product
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.psd_cauchy_schwarz
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.rCount
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.result
• Truth anchor: D5/S3/Quantum/Measurement/DetectorSensorDickeOptimality.weight_class_card
• Dependency: D5/S3/Quantum/Entanglement/TriangleIndependentSourceNoise
• Dependency: D5/S3/Quantum/Measurement/AntidistinguishabilityGram
• Dependency: D5/S3/Quantum/Recovery/PurifiedLocalPath
• Dependency: D5/S3/Quantum/Reduction/IsometricCompression