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
- , outcomes , , and with .
- 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))$.
- The pair , has and .
- 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:
probeOpis andmultiProbeOpits -fold tensor product, written entrywise on the product basis;gammais Eq. (AgammaN) with and ; it takes the real part of each summand, whose numerator and denominator are real in the source;basisPower jis , andcatState,catPerpare 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,witnessPerpandresult. - Reuse:
multiProbeOpapplies the frozenpiKroneckerLinearEquivofPrimePowerTensorTowerto the tensor product of the single-probe matrices; the proof reads its entries through the frozenpi_kronecker_linear_equiv_tprod_single. - Freeze identities:
- module statement
sha256:1813e7c39fe2a203ddc3ae4017060513573094dcfe5c615d808cbfeb254ceae8; resultstatementsha256:776162f0773ebb482186286dec12dab90a961361f14c4ded6b203265e197a2d4;- Freeze event
sha256:e9a83ae15dc54838881c4bbea6e3f6511547f4ec9af1deb44dacc56b37652895. Its project-level frozen prerequisite is the Freeze event ofPrimePowerTensorTower,sha256:a719804d007bf8a687cc502c902f7437de1d8a2e8bb55f372b057e9c0afbec3a.
- module statement
- Axioms: the proof uses only
propext,Classical.choiceandQuot.sound. It contains nosorry, nonative_decideand 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, basisrefutesthe module’sclaim.
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.