slug: divianszky-et-al-2023-lk-bound-nontightness
bibkey: divianszkymartonbenevertesi2023certification
doi: 10.1038/s41598-023-39529-0
url: https://arxiv.org/abs/2211.17185v2
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Optimization/PrepareMeasureLkBound.result

The bound L_k(M) ≤ k L(M) is not tight for k ≥ 3

Problem

P. Diviánszky, I. Márton, E. Bene and T. Vértesi, Certification of qubits in the prepare-and-measure scenario with large input alphabet and connections with the Grothendieck constant, arXiv:2211.17185v2 (Sci. Rep. 13, 13200, 2023), Methods, after Lemma III.4:

It is an open question whether Lemma~\ref{LkkL} is tight or not.

Hence, for $k=2$ the upper bound in Lemma~\ref{LkkL} is tight. We conjecture that the bound is not tight for greater values of $k$.

Here, for a real $n\times m$ matrix $M$:

• $L(M)={\max }_{v\in \{\pm 1{\}}^n}\Vert vM{\Vert }_1$, the classical bound of the correlation expression $M$;
• $L_k(M)={\max }_W{\sum }_i\Vert (W^{\mathsf{T}}M{)}_i{\Vert }_1$ over the $n\times k$ matrices $W$ whose rows are standard basis vectors, which groups the inputs into $k$ classes;
• Lemma III.4 states $L_k(M)\le kL(M)$.

The definitions are quoted in the literature note.

Issue #20049 fixes the reading: for every $k\ge 3$ there is $c_k<k$ with $L_k(M)\le c_{k}L(M)$ for all matrices. This is proved.

Motivation

The source certifies qubits in prepare-and-measure experiments by comparing quantum values with $L_k(M)$, the best value achievable with $k$-valued classical messages, and relates the resulting constants to the Grothendieck constant of order 3. Lemma III.4 bounds $L_k(M)$ by $k$ times the sign-vector bound $L(M)$; its tightness decides whether the factor $k$ in the certification thresholds can be improved.

Gap

The literature check before any Lean is recorded in #20049:

• the v2 TeX keeps the question and the conjecture;
• the search seat read the ten citing works listed by Semantic Scholar and found no settlement or improved constant;
• the repository had no record.

not-found-in-searched-scope.

Route

Put $a_k=2^{-k}{\sum }_{\epsilon \in \{\pm 1{\}}^k}|{\sum }_i{\epsilon }_i|$.

1. The averaged norm. $g(x)=2^{-k}{\sum }_{\epsilon }|{\sum }_i{\epsilon }_i{x}_i|$ is convex and invariant under sign changes and permutations, so $g(x)\ge (a_k/k){\sum }_i|x_i|$.
2. Comparison. For $B=W^{\mathsf{T}}M$ and each $\epsilon$, the row ${\epsilon }^{\mathsf{T}}{W}^{\mathsf{T}}$ is a sign vector, so $\Vert {\epsilon }^{\mathsf{T}}B{\Vert }_1\le L(M)$. Averaging over $\epsilon$ gives $L(M)\ge (a_k/k){\sum }_i\Vert B_i{\Vert }_1$, hence $L_k(M)\le (k/a_k)L(M)$.
3. The constant. $a_3=3/2$ and $a_k$ is nondecreasing, so $k/a_k\le 2k/3<k$ for $k\ge 3$.

Falsifier

The proof would not answer the conjecture if the module’s quantities differed from the source’s. The module:

• encodes each matrix in $W_{n,k}$ by its row map $f:\mathrm{Fin}n\to \mathrm{Fin}k$, the matrix whose $i$-th row is $e_{f(i)}$, and defines the Manhattan norm, $L_k$ and $L$ as the source’s Methods section does;
• proves a uniform constant below $k$, which excludes both a matrix with $L(M)>0$ attaining $L_k=kL$ and a sequence approaching ratio $k$.

Evidence

The canonical source is D5/S3/Quantum/Optimization/PrepareMeasureLkBound.lean (295 lines).

• Proof. It proves result : claim.
• Axioms. It uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Frozen state: Golden/Frozen/state/D5/S3/Quantum/Optimization/PrepareMeasureLkBound.lean.json, statement sha256:35869074c43c870335cbd81aa1464350253c4c8cc362cc35c8c2fa500f09b773.

Declaration statements:

• result: sha256:7d6d5b60f9968f28ae22a6b1a4dca7efc9ff69c08dcf001518b41265a47026ef;
• claim: sha256:73c662c788f9fad8b43af8ba4ea5a77bd496b6953d39b433c1dd1175737899e8.

Triage

Tier 1 conjecture of a 2022 preprint kept in the 2023 journal version, preregistered in issue #20049 before any Lean. theorem; resolution proved.

The module is admitted under the open-problem-resolution basis of CLAUDE.md §3.2; the per-declaration proof shapes are listed in the delivery PR. There is no digestion atom.

What the settlement shows

Proved by result: for every $k\ge 3$, $L_k(M)\le c_{k}L(M)$ with a constant $c_k<k$, for all real matrices.

Computed, not formalized (orchestrator, brute force, recorded in #20049):

• The constant. For $k=2,3,4$ and 900 random matrices, $L_k/L$ never exceeds $k/a_k$ ($2$, $2$, $8/3$).
• Sharpness. The $k\times 2^k$ matrix whose columns are all sign vectors attains $L_k/L=k/a_k$ for $k=3,4$.
• The source’s family is extremal. The source evaluates $L_k(M^{(k)})/L(M^{(k)})=2^{k-1}/\left(\genfrac{}{}{0ex}{}{k-1}{\lfloor (k-1)/2\rfloor }\right)$ for its family $M^{(k)}$. Exact rational arithmetic gives $k/a_k=2^{k-1}/\left(\genfrac{}{}{0ex}{}{k-1}{\lfloor (k-1)/2\rfloor }\right)$ for $k=2,\dots ,13$, so on that range the proved constant is attained by the source’s own matrices and is optimal.

Argued, not formalized.

• Mechanism. Grouping the inputs into $k$ classes and taking the ${\ell }_1$ norm of each class sum can beat a single sign assignment by at most the ratio of the ${\ell }_1$ norm to the average random-sign norm, which is $k/a_k$ rather than $k$. For $k=2$, $a_2=1$ and the bound is $2=k$, matching the CHSH case.
• Growth. $a_k=\mathbb{E}|{\epsilon }_1+\cdots +{\epsilon }_k|\sim \sqrt{2k/\pi }$, so the optimal constant grows like $\sqrt{\pi k/2}$ instead of $k$.
• The identity behind extremality. $a_k=k\left(\genfrac{}{}{0ex}{}{k-1}{\lfloor (k-1)/2\rfloor }\right)/2^{k-1}$ is the classical formula for the mean absolute value of a simple random walk; it turns the computed equality into an identity for every $k$.
• Effect on the paper. The factor $k$ in Lemma III.4 can be replaced by $k/a_k$, which improves every threshold that uses the lemma.

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty or priority; the citing works were read by the search seat. The statements in “Computed, not formalized” and “Argued, not formalized” are not formalized; sharpness for $k\ge 5$ was not computed.