Metadata

slug: zhang-et-al-2019-qubit-incompatibility-probability
bibkey: zhang2019incompatibilityprobability
doi: 10.1103/PhysRevE.100.062139
url: https://arxiv.org/abs/1912.12321
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Measurement/QubitIncompatibilityProbability.result

The incompatibility probability of random qubit measurements

Problem

L. Zhang, H. Xiang, X. Li-Jost and S.-M. Fei, Incompatibility probability of random quantum measurements, Phys. Rev. E 100, 062139, arXiv:1912.12321, Section III.C, PDF p. 5, states:

We conjecture that the incompatibility probability of a pair of random qubit measurements $A$ and $B$ , generated by $(a_{0}, a)$ and $(b_{0}, b)$ in Eq. (4), is given by $Pr [Θ_{2, 2}^{NJM}] = \frac{1}{4} .$

Issue #15842 fixes the literal statement, the squared-form criterion and the source and literature boundaries.

Statement echo

Source clause	Lean counterpart	Fidelity
Uniform random qubit observables in $V = {(x_{0}, x) : ∣ x_{0} ∣ + ∥ x ∥ \leq 1}$	`OrderedRootCoordinates.V` on $R \times R^{3}$	The entire closed body is retained.
Yu–Liu–Li–Oh square-root function	`OrderedRootCoordinates.hYu`	Both $(1 + x_{0})^{2}$ and $(1 - x_{0})^{2}$ occur under the square roots.
The set of pairs violating Eq. (4)	`OrderedRootCoordinates.NJM`	Both body memberships and the strict violation of the squared criterion are retained.
Product Lebesgue volume divided by $vol (V)^{2}$	`OrderedRootCoordinates.incompProb`	The measure is actual product Lebesgue measure.
Probability equals $1/4$	`OrderedRootCoordinates.claim`	Literal equality, without extra hypotheses.
Negation of the conjecture	`QubitIncompatibilityProbability.result`	Unconditional negation of that claim.

The main-text display of $h$ omits squares on $1 \pm x_{0}$ . The squared form is the expression in Appendix C and in Yu–Liu–Li–Oh, Eq. (5), arXiv:0805.1538. The formal definitions use that preregistered squared form. The strict-interior coordinate maps are smooth bijections; the closed body is not replaced by an interior in the claim. Body boundaries, zero vectors and cosine endpoints are removed only within the integration proof, where their nullity is proved.

Motivation

D5/S3/Quantum/Measurement/QubitIncompatibilityProbability.result refutes the conjecture. The exact reduction and certificate in its proof give

$Pr = 9 I \leq \frac{5910272}{23648625} = \frac{1}{4} - \frac{7537}{94594500} < \frac{1}{4} .$

Here

$I = 4 \int_{[0, 1]^{4}} ρ^{3} 1 - ρ α (1 - α) (1 - t^{2}) (1 - s^{2}) 1 - ρ (α t^{2} + (1 - α) s^{2}) d ρ d α d t d s .$

No atom or coverage claim is involved. The two supporting modules provide the coordinate inverse constructions on the refutation’s dependency path.

Gap

The source and literature checks in #15842 are attributed to the ChatGPT Pro search producer and the Claude Code orchestrator. Six of the seven counted citing works were identified and checked in the supplied literature screen; the seventh remains unidentified. Those checks do not establish exhaustive publication-priority clearance. The reported numerical value alone is not the refutation: the strict rational upper bound is proved by Lean.

Route

OrderedRootCoordinates.root_coordinates identifies the squared Yu factors in ordered-root coordinates, and angular_volume_ordered computes the incompatible angular interval. coordinate_change_lintegral uses the explicit inverse coordinateMap_surjective to transfer volume over the strict interiors. volume_NJM_four_sectors, body_boundary_null and vector_zero_null restore the complete original body.

QubitIncompatibilityRadialReduction.volume_NJM_rootI combines relative-cosine integration with the ordered-root Jacobian. Its inverse construction meridian_surjective supplies the meridian change of variables. The radial factors cancel, giving incompatible volume $4 π^{2} rootI$ .

Within QubitIncompatibilityProbability, rootI_eq_squareI, squareI_eq_cubeL and cubeL_eq_ofReal_integral convert that nonnegative integral to the real cube integral. incompProb_eq_nine_I establishes $Pr = 9 I$ . The polynomial $p (z) = 1 - z /2 - z^{2} /8$ bounds $1 - z$ on $[0, 1]$ . radial_moment_B0, radial_moment_B1, radial_moment_B2 and polynomial_cube_integral give the explicit moment certificate; cube_integral_upper_bound and incompProb_upper_bound yield the rational separation, which result uses to negate the claim. These settling-module helper theorems are private.

Falsifier

A transcription discrepancy in $V$ , the squared $h$ , the incompatible set or the product-volume probability would invalidate source fidelity. A discrepancy in a change-of-variables hypothesis, null-set exclusion or the moment certificate would invalidate the proposed route. A prior publication settling the same conjecture would invalidate the unsettled-problem premise, without changing the kernel-checked theorem.

Evidence

The three Lean modules and their Scribes supply the mathematical evidence. Every public declaration’s axiom closure is contained in ${propext, Classical.choice, Quot.sound}$ . The public settling theorem is exactly the negation of the source-faithful claim.

Four-slot escape registration is unfinished for all ten new public theorems, including result: #15930. The headers carry utility: none, so the refutation has no registration exemption. The searched enrolled equality, order, guarded equality, iff, existential-witness and dependent-family templates do not supply this delivery’s faithful source reconstruction, realization/readout bridges, whole-family sensitivity and observational dependence. No Reg source or validated registration is asserted.

Experiment entry

The numerical program is in the experiment entry pinned to b0dd9513c26f1d8aa73f8a1be883da2f5ce480ac. Command: python3 check.py from that directory; exit 0. The script SHA-256 is 65864e35d385fccc7911d1b8791bd319d68c8770fe850bdd94fa4615c96c408e.

Exact fraction arithmetic recomputes the three radial moments and the three angular moments and obtains $5910272/23648625$ ; the square-root inequality is also checked on 100001 grid points. Tensor Gauss–Legendre quadrature uses $4 8^{4}$ nodes after $ρ = 1 - z^{2}$ and gives $9 I = 0.24960602817387387$ . Monte Carlo uses seed 1912 and 20000000 independent uniform pairs in the original parameter bodies; it gives $0.24960 \pm 0.00010$ , with the uncertainty equal to the binomial standard error. The script reports zero failed checks. These finite numerical checks do not establish a closed form or a uniform error theorem for quadrature.

Triage

What the settlement shows

Lane target	Status and evidence kind	Result and boundary
Ordered-root mechanism and contained angular interval	Proved, kernel-checked: `OrderedRootCoordinates.root_coordinates`, `angular_volume_ordered`, `coordinate_change_lintegral`	The Yu factors and the exact angular volume follow on the ordered-root interior; null-set arguments restore the complete body.
Cancellation and exact probability $9 I$	Proved, kernel-checked: `QubitIncompatibilityRadialReduction.volume_NJM_rootI`; private `QubitIncompatibilityProbability.volume_NJM_cubeI` and `incompProb_eq_nine_I`	Relative-cosine integration cancels the radial factors, and normalization gives the exact four-dimensional integral.
Degree-two bound and three explicit moments	Proved, kernel-checked: private `sqrt_certificate`, `radial_moment_B0`, `radial_moment_B1`, `radial_moment_B2`, `polynomial_cube_integral`, `cube_integral_upper_bound`, `incompProb_upper_bound`; public `result`	$Pr \leq 5910272/23648625 < 1/4$ , hence the conjecture is false.
Quadrature and Monte Carlo readings	Computed, the pinned experiment entry above, exit 0 and the stated SHA-256	Quadrature $9 I = 0.24960602817387387$ at $4 8^{4}$ nodes; Monte Carlo $0.24960 \pm 0.00010$ over 20000000 pairs. Their tested scopes are finite.
Exact closed form of $I$	Open	The integral identity and strict rational bound do not evaluate $I$ in closed form.
Higher-dimensional analogous probabilities	Open	The proof uses the three-dimensional Bloch vector of a qubit and does not extend to higher-dimensional observables.
Analogous unbiased-qubit probabilities	Open for other distributions and families	The source’s Theorem 2 already proves $3/5$ for its uniform unbiased pair ensemble; that paper result is independent of the one-quarter conjecture and is not a new Lean result here.
Seventh citing work	Open, ASSUMED-UNVERIFIED literature reading	The supplied seven-citation count has only six identified works; no priority clearance is inferred.

The failure mechanism is the exact ordered-root angular interval and its integrated density: the polynomial-moment certificate places the complete biased-qubit probability strictly below $1/4$ . The nearest surviving statements are the exact integral formula and rational upper bound. The source’s independent unbiased-qubit calculation survives; other source results are not re-established by this refutation, and no claim about consequences outside the conjecture’s dependency scope is made.

ASSUMED-UNVERIFIED

Publication novelty and priority remain unverified because the seventh counted citing work is unidentified and the supplied literature screen is not exhaustive.
The integral’s closed form and the stated neighbouring probability problems are open within this delivery’s scope.
Four-slot escape audit remains unfinished under #15930; kernel verification and frozen membership do not supply its missing registration evidence.

trureturing — Discovering truth