Ordered Root Coordinates

Abstract

Ordered roots describe the exact angular incompatibility interval.

Definition 1.1 (Qubit parameter body).

$$V=\{p:(\mathbb{R}\times \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))\mid \left|(p).1\right|+\Vert (p).2\Vert \le 1\}$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.V (✓ std3).

Citation. Lin Zhang; Hua Xiang; Xiao Li-Jost; Shao-Ming Fei (2019). Incompatibility probability of random quantum measurements. DOI: 10.1103/PhysRevE.100.062139. URL: https://arxiv.org/abs/1912.12321.

Commentary.

Section III, p. 3, uses V = {(x₀, x) ∈ R⁴ : |x₀| + |x| ≤ 1}. The vector carrier is EuclideanSpace R (Fin 3); the first component is the bias.

Definition 1.2 (Yu function).

$$\forall x:\mathbb{R},\forall a:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right),\mathrm{hYu}\left(x,a\right)=\frac{Real.sqrt\left((1+x{)}^2-(\Vert a\Vert {)}^2\right)+Real.sqrt\left((1-x{)}^2-(\Vert a\Vert {)}^2\right)}{2}$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.hYu (✓ std3).

Citation. Sixia Yu; Nai-le Liu; Li Li; C. H. Oh (2010). Joint measurement of two unsharp observables of a qubit. DOI: 10.1103/PhysRevA.81.062116. URL: https://arxiv.org/abs/0805.1538.

Commentary.

Yu, Liu, Li and Oh, Eq. (5), p. 2, and Zhang et al., Appendix C, use squares on 1 ± x under the square roots.

Definition 1.3 (Incompatible measurement pairs).

$$NJM=\{q:((\mathbb{R}\times \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))\times (\mathbb{R}\times \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)))\mid ((q).1\in V)\wedge (((q).2\in V)\wedge ((\mathrm{inner}\left(\mathbb{R},((q).1).2,((q).2).2\right)-(((q).1).1)\cdot (((q).2).1){)}^2<(1-(\mathrm{hYu}\left(((q).1).1,((q).1).2\right){)}^2-(\mathrm{hYu}\left(((q).2).1,((q).2).2\right){)}^2)\cdot (1-\frac{(((q).1).1{)}^2}{(\mathrm{hYu}\left(((q).1).1,((q).1).2\right){)}^2}-\frac{(((q).2).1{)}^2}{(\mathrm{hYu}\left(((q).2).1,((q).2).2\right){)}^2})))\}$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.NJM (✓ std3).

Citation. Lin Zhang; Hua Xiang; Xiao Li-Jost; Shao-Ming Fei (2019). Incompatibility probability of random quantum measurements. DOI: 10.1103/PhysRevE.100.062139. URL: https://arxiv.org/abs/1912.12321.

Commentary.

Section III.C, p. 5: “can be identified as the set that Eq. (4) is violated.” Both points belong to V, and the strict inequality is the violation of the joint-measurability criterion.

Definition 1.4 (Incompatibility probability).

$$incompProb=\frac{ENNReal.toReal\left(MeasureTheory.volume\left(NJM\right)\right)}{(ENNReal.toReal\left(MeasureTheory.volume\left(V\right)\right){)}^2}$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.incompProb (✓ std3).

Citation. Lin Zhang; Hua Xiang; Xiao Li-Jost; Shao-Ming Fei (2019). Incompatibility probability of random quantum measurements. DOI: 10.1103/PhysRevE.100.062139. URL: https://arxiv.org/abs/1912.12321.

Commentary.

Section III.C, p. 5, defines the probability as the incompatible volume divided by the volume of the full parameter body V × V. All volumes are product Lebesgue volumes.

Definition 1.5 (One-quarter conjecture).

$$(claim)\iff (incompProb=\frac{1}{4})$$

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

Citation. Lin Zhang; Hua Xiang; Xiao Li-Jost; Shao-Ming Fei (2019). Incompatibility probability of random quantum measurements. DOI: 10.1103/PhysRevE.100.062139. URL: https://arxiv.org/abs/1912.12321.

Commentary.

Section III.C, PDF p. 5: We conjecture that the incompatibility probability of a pair of random qubit measurements $\mathbf{A}$ and $\mathbf{B}$, generated by (a₀, 𝒂) and (b₀, 𝒃) in Eq. (4), is given by 𝐏𝐫[Θᴺᴶᴹ₂,₂] = $\frac{1}{4}$. Here claim says that the real-valued probability equals one quarter.

Definition 1.6 (Positive biases).

$$positiveSector=Set.inter\left(NJM,\{q:((\mathbb{R}\times \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))\times (\mathbb{R}\times \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)))\mid (0<((q).1).1)\wedge (0<((q).2).1)\}\right)$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.positiveSector (✓ std3).

Source. Repository-derived.

Commentary.

Both bias coordinates are strictly positive.

Theorem 1.7 (Body volume).

$$MeasureTheory.volume\left(V\right)=ENNReal.ofReal\left(\frac{(2)\cdot (Real.pi)}{3}\right)$$

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

Citation. Lin Zhang; Hua Xiang; Xiao Li-Jost; Shao-Ming Fei (2019). Incompatibility probability of random quantum measurements. DOI: 10.1103/PhysRevE.100.062139. URL: https://arxiv.org/abs/1912.12321.

Commentary.

Section III, p. 3, gives the volume of V as 2π/3.

Theorem 1.8 (Four equal sectors).

$$MeasureTheory.volume\left(NJM\right)=(4)\cdot (MeasureTheory.volume\left(positiveSector\right))$$

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

Source. Repository-derived.

Commentary.

Negating either measurement preserves the criterion; zero bias slices have zero volume.

Theorem 1.9 (Null body boundary).

$$MeasureTheory.volume\left(\{p:(\mathbb{R}\times \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))\mid \left|(p).1\right|+\Vert (p).2\Vert =1\}\right)=0$$

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

Source. Repository-derived.

Commentary.

The boundary |x| + norm(a) = 1 has zero volume.

Theorem 1.10 (Null zero-vector slice).

$$MeasureTheory.volume\left(\{p:(\mathbb{R}\times \mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))\mid (p).2=0\}\right)=0$$

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

Source. Repository-derived.

Commentary.

The subset with zero vector has zero volume.

Definition 1.11 (Bias coordinate).

$$\forall u:\mathbb{R},\forall v:\mathbb{R},\mathrm{xCoord}\left(u,v\right)=(Real.sqrt\left(u\right))\cdot (Real.sqrt\left(v\right))$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.xCoord (✓ std3).

Source. Repository-derived.

Commentary.

The bias coordinate is sqrt(u) times sqrt(v).

Definition 1.12 (Radius coordinate).

$$\forall u:\mathbb{R},\forall v:\mathbb{R},\mathrm{rCoord}\left(u,v\right)=(Real.sqrt\left(1-u\right))\cdot (Real.sqrt\left(1-v\right))$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.rCoord (✓ std3).

Source. Repository-derived.

Commentary.

The radius is sqrt(1-u) times sqrt(1-v).

Theorem 1.13 (Criterion coordinates).

$$\forall u:\mathbb{R},\forall v:\mathbb{R},((0\le v)\wedge ((v\le u)\wedge (u\le 1)))\Rightarrow ((0<u)\Rightarrow (((\mathrm{hYu}\left(\mathrm{xCoord}\left(u,v\right),PiLp.single\left(2,0,\mathrm{rCoord}\left(u,v\right)\right)\right){)}^2=u)\wedge (\frac{(\mathrm{xCoord}\left(u,v\right){)}^2}{(\mathrm{hYu}\left(\mathrm{xCoord}\left(u,v\right),PiLp.single\left(2,0,\mathrm{rCoord}\left(u,v\right)\right)\right){)}^2}=v)))$$

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

Source. Repository-derived.

Commentary.

For ordered roots, the squared Yu function is u and the squared bias divided by u is v.

Theorem 1.14 (Exact angular interval volume).

$$\forall u:\mathbb{R},\forall v:\mathbb{R},\forall U:\mathbb{R},\forall V:\mathbb{R},((0\le v)\wedge ((v\le u)\wedge (u\le 1)))\Rightarrow (((0\le V)\wedge ((V\le U)\wedge (U\le 1)))\Rightarrow (MeasureTheory.volume\left(\{s:\mathbb{R}\mid (-1\le s)\wedge ((s\le 1)\wedge ((((\mathrm{rCoord}\left(u,v\right))\cdot (\mathrm{rCoord}\left(U,V\right)))\cdot (s)-(\mathrm{xCoord}\left(u,v\right))\cdot (\mathrm{xCoord}\left(U,V\right)){)}^2<(1-u-U)\cdot (1-v-V)))\}\right)=\mathrm{ite}\left(0<1-u-U,ENNReal.ofReal\left(\frac{(2)\cdot (Real.sqrt\left((1-u-U)\cdot (1-v-V)\right))}{(\mathrm{rCoord}\left(u,v\right))\cdot (\mathrm{rCoord}\left(U,V\right))}\right),0\right)))$$

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

Source. Repository-derived.

Commentary.

Only 1-u-U > 0 contributes. In that region the incompatible cosine interval lies entirely in [-1,1].

Definition 1.15 (Ordered-root map).

$$\forall p:(\mathbb{R}\times \mathbb{R}),\mathrm{coordinateMap}\left(p\right)=(\mathrm{xCoord}\left((p).1,(p).2\right),\mathrm{rCoord}\left((p).1,(p).2\right))$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.coordinateMap (✓ std3).

Source. Repository-derived.

Commentary.

The two coordinates are the bias and radius.

Definition 1.16 (Strictly ordered roots).

$$rootDomain=\{p:(\mathbb{R}\times \mathbb{R})\mid (0<(p).2)\wedge (((p).2<(p).1)\wedge ((p).1<1))\}$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.rootDomain (✓ std3).

Source. Repository-derived.

Commentary.

The roots satisfy 0 < v < u < 1.

Definition 1.17 (Strict radial body).

$$radialBody=\{p:(\mathbb{R}\times \mathbb{R})\mid (0<(p).1)\wedge ((0<(p).2)\wedge ((p).1+(p).2<1))\}$$

Formalization. D5/S3/Quantum/Measurement/OrderedRootCoordinates.radialBody (✓ std3).

Source. Repository-derived.

Commentary.

The bias and radius are positive and their sum is less than one.

Theorem 1.18 (Measurability of the root domain).

$$\mathrm{MeasurableSet}\left(rootDomain\right)$$

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

Source. Repository-derived.

Commentary.

The strict root inequalities define a measurable set.

Theorem 1.19 (Ordered-root change of variables).

$$\forall f:(\mathbb{R}\times \mathbb{R})\to ENNReal,{\int }_{p:(\mathbb{R}\times \mathbb{R})\in radialBody}^{-}(f\left(p\right))dMeasureTheory.volume={\int }_{p:(\mathbb{R}\times \mathbb{R})\in rootDomain}^{-}((ENNReal.ofReal\left(\frac{(p).1-(p).2}{((4)\cdot (\mathrm{xCoord}\left((p).1,(p).2\right)))\cdot (\mathrm{rCoord}\left((p).1,(p).2\right))}\right))\cdot (f\left(\mathrm{coordinateMap}\left(p\right)\right)))dMeasureTheory.volume$$

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

Source. Repository-derived.

Commentary.

The absolute Jacobian is (u-v)/(4 xCoord(u,v) rCoord(u,v)). The identity holds for nonnegative extended-real integrands.

References

• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.NJM
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.V
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.angular_volume_ordered
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.body_boundary_null
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.claim
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.coordinateMap
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.coordinate_change_lintegral
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.hYu
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.incompProb
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.measurableSet_rootDomain
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.positiveSector
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.rCoord
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.radialBody
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.rootDomain
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.root_coordinates
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.vector_zero_null
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.volume_NJM_four_sectors
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.volume_V
• Truth anchor: D5/S3/Quantum/Measurement/OrderedRootCoordinates.xCoord