Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: len-2022-noisy-metrology-cat-optimality
bibkey: len2022quantum
doi: 10.1038/s41467-022-33563-8
url: https://arxiv.org/abs/2109.01160v2
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Measurement/NoisyMeasurementCatOptimalityRefutation.result

Optimality of cat pairs for metrology with noisy measurements

Problem

Y. L. Len, T. Gefen, A. Retzker and J. Kołodyński, Quantum metrology with imperfect measurements, Nature Communications 13, 6971 (2022), arXiv:2109.01160v2. An imperfect measurement multiplies the quantum Fisher information by

and for probes measured independently $M_{\xvec}=M_{x_1}\otimes\cdots\otimes M_{x_N}$. The supplement conjectures:

for any classical noise channel, that is applied independently on each of the probes, the optimal take the form of ``cat states“: $|\zeta^{N} \rangle =\cos\left(\theta\right)|j\rangle^{\otimes N}+\sin\left(\theta\right)|k\rangle^{\otimes N}$, $|\zeta_{\perp}^{N} \rangle =-\sin\left(\theta\right)|j\rangle^{\otimes N}+\cos\left(\theta\right)|k\rangle^{\otimes N}$

Here are the images of under the encoding unitary, so the optimized pair is , .

Motivation

The conjecture would reduce the optimal noisy-readout protocol for probes to a single-probe choice of two levels and one angle. The frozen declaration D5/S3/Quantum/Measurement/NoisyMeasurementCatOptimalityRefutation.result shows that no cat pair need be optimal.

Gap

Issue #12917 classifies the conjecture as Tier 1. Before any Lean it recorded the following checks:

  • Zhou, Michalakis and Gefen, PRX Quantum 4, 040305 (2023), arXiv:2210.11393v3, Theorem 6: for commuting measurements some optimal pair is supported on two common-eigenbasis states of the whole system, that is, on two arbitrary words. Their symmetric bit-flip example has non-repeated co-optimal words while repeated words remain optimal, and they leave the choice of words open.
  • The objective is the Le Cam divergence of a binary-input channel (Polyanskiy–Wu 2017, App. B; Ordentlich–Polyanskiy 2022). Neither source compares repeated with non-repeated words.
  • QIQCOP Zoo and this repository have no record of the paper or of the claim.

These are seat-reported readings checked against the cited theorems’ statements, not-found-in-searched-scope; they do not establish exhaustive worldwide novelty.

Route

  1. , outcomes , , and with .
  2. Write . For orthonormal real vectors supported on two words , with having squared weight on , $\gamma=\sum_{\mathbf x}t(1-t)(m_{\mathbf x}(u)-m_{\mathbf x}(v))^2/ (t,m_{\mathbf x}(u)+(1-t),m_{\mathbf x}(v))$.
  3. The pair , has and .
  4. A cat pair with has , and . Each summand equals with , and for , so is at most an affine function of . At and it is below for , , , , , on the ordered pairs , , , , , .

Falsifier

The kernel-checked result is the negation of the following statement. For every , every finite type , every with and , and every , there are in and such that every orthonormal pair of vectors on the words has . The definitions are as follows:

  • probeOp is and multiProbeOp its -fold tensor product, written entrywise on the product basis;
  • gamma is Eq. (AgammaN) with and ; it takes the real part of each summand, whose numerator and denominator are real in the source;
  • basisPower j is , and catState, catPerp are the displayed cat pair.

With all every is positive definite, so is continuous on the compact set of orthonormal pairs and attains its maximum (orchestrator reasoning, not in Lean); the conjecture’s “the optimal” pair presupposes one. With zero entries the maximum need not be attained (seat-reported: Zhou–Michalakis–Gefen, arXiv:2210.11393v3, the assumption before Theorem 6 and its appendix), and the encoding does not treat that case.

Evidence

  • Values (Python fractions, exact): the witness value is ; the six tangent bounds are below .
  • Numerical scan of this detector (double precision, all pairs of words, on a grid of step ):
    • : the best pair is a cat pair;
    • : best at the words , against for repeated words;
    • : best at , against .

The canonical source is D5/S3/Quantum/Measurement/NoisyMeasurementCatOptimalityRefutation.lean.

  • Public declarations: probeOp, multiProbeOp, gamma, basisPower, catState, catPerp, claim, detector, witness, witnessPerp and result.
  • Reuse: multiProbeOp applies the frozen piKroneckerLinearEquiv of PrimePowerTensorTower to the tensor product of the single-probe matrices; the proof reads its entries through the frozen pi_kronecker_linear_equiv_tprod_single.
  • Freeze identities:
    • module statement sha256:1813e7c39fe2a203ddc3ae4017060513573094dcfe5c615d808cbfeb254ceae8;
    • result statement sha256:776162f0773ebb482186286dec12dab90a961361f14c4ded6b203265e197a2d4;
    • Freeze event sha256:e9a83ae15dc54838881c4bbea6e3f6511547f4ec9af1deb44dacc56b37652895. Its project-level frozen prerequisite is the Freeze event of PrimePowerTensorTower, sha256:a719804d007bf8a687cc502c902f7437de1d8a2e8bb55f372b057e9c0afbec3a.
  • Axioms: the proof uses only propext, Classical.choice and Quot.sound. It contains no sorry, no native_decide and no new axiom.

Triage

Tier 1 conjecture of a 2022 journal article. Resolution: Refuted, by D5/S3/Quantum/Measurement/NoisyMeasurementCatOptimalityRefutation.result.

  • proof_shape: bind-only. The settlement of the named conjecture is the new content; there is no escape witness.
  • admission_basis: open-problem-resolution (issue #12917).
  • Utility kind certified-instance, basis refutes the module’s claim.

What the settlement shows

  • Proved by result: for the stated qutrit detector and two probes, the pair has a larger than every cat pair, so no cat pair is optimal.
  • Proved inside the proof of result: the formula for of any real orthonormal pair supported on two words, and a tangent-line upper bound for when .
  • Mechanism (orchestrator reading, not stated in Lean): by step 2, a pair on two words is scored by the Le Cam divergence of the two product distributions. Repeated words , use the same label pair on both probes; crossed words such as , use the label pairs and on the two probes. For this detector the crossed product distributions have the larger divergence (steps 3 and 4).
  • Effect on the paper’s other conclusions (read from the arXiv source):
    • Lemma 1 and Theorem 1, the convergence of the noisy QFI to the perfect QFI as , are unaffected; the example concerns only which pair attains at finite .
    • The Hellinger-distance statement earlier in the same paragraph is unaffected: Bhattacharyya coefficients multiply over probes, so a repeated pair of the best single-probe labels minimizes them (orchestrator reasoning, not in Lean).
    • At , for detectors with all , Zhou–Michalakis–Gefen Theorem 6 gives an optimal pair of the form , on two basis states. The inverse change of variables , turns it into a real rotation of , which is a cat pair; so the conjecture holds for one probe under that assumption (seat-reported reading of the theorem statement).
  • Open here:
    • the qubit specialization of the paper (, labels );
    • for which detectors and which cat pairs fail;
    • whether the gap persists for all for this detector, beyond the reading above.

ASSUMED-UNVERIFIED

The literature checks do not establish worldwide priority; the journal supplement’s wording is seat-reported, and the quotations are from the arXiv v2 source. The Lean kernel verifies the encoded statement and its axiom closure. Its correspondence to the paper, including the real part in gamma and the weakest reading of “optimal”, is checked by reading the source and the definitions.