slug: cotfas-2026-uncertainty-condition-conjecture
bibkey: cotfas2026dvgs
doi: 10.48550/arXiv.2610.05623
url: https://arxiv.org/abs/2610.05623v1
triage: theorem
motivation_gids:
  - D5/S3/Quantum/CotfasDVGS.result

The uncertainty condition suffices for the mixed discrete Gaussian

Problem

Nicolae Cotfas, Frame-dependent coherence of Gaussian quantum states, arXiv:2610.05623v1, asks after Eq. (22): “As concern ρ̃_σ, we do not know if (11) is sufficient in order to have ρ̃_σ ≥ 0. Based on our numerical investigations, we conjecture that this is true.”

Preregistration #18946 fixes the source formulas and quantifiers. The source note gives the locators and verbatim statements. The settlement is Proved by D5.S3.Quantum.CotfasDVGS.result.

Statement echo

The public surface comprises W, parity, wSum, unnormalized, rhoTilde, claim and result. All other authored declarations are private and have consumers inside this settlement. The centered index type and density conjunction occur literally in the claim; the proof uses existing covariance and density predicates.

Motivation

A trace-normalized mixed discrete-variable Gaussian can serve as a quantum state when it is positive semidefinite. The theorem supplies that density-operator premise for the exact family in Eqs. (21)–(22), including the determinant-one boundary. It establishes no separate result about coherence quantities or other conclusions of the paper.

Gap

The source states the sufficiency question explicitly. The literature screen recorded in #18946 covers arXiv:2610.05623v1, the predecessor arXiv:2204.07042v4, INSPIRE citing-work abstracts, indexed MathDB searches and the formal-conjectures snapshot named there. It found no settlement in that scope. Direct MathDB access returned HTTP 403; Feng–Luo, International Journal of Theoretical Physics 63, 40 (2024), has a subscription-only main text in which an equivalent result has not been excluded. Literature completeness is ASSUMED-UNVERIFIED.

Route

Write $a={\sigma }_{00}$, $c={\sigma }_{01}$ and $D=\det \sigma$. The consumed covariance result GaussianThermometryJointMeasurementRefutation.physical_data gives $D\ge 1$ from the uncertainty condition. rhoTilde_scaling reduces the Planck parameter to $d$.

The private kernel_identity identifies the unnormalized matrix with twice the integer periodization of

$$K(x,y)=\sqrt{\frac{2}{da}}\exp \left(-\frac{\pi ((x+y{)}^2+D(x-y{)}^2)}{2da}+\frac{i\pi c(x^2-y^2)}{da}\right).$$

The private half_lattice_poisson applies Mathlib’s Complex.tsum_exp_neg_quadratic. The reindexing and Gaussian summability arguments justify the exact signed Wigner construction. kernel_factorization writes $K(x,y)=g(x)\overline{g(y)}{e}^{-\lambda (x-y{)}^2}$, where $\lambda =\pi (D-1)/(2da)\ge 0$. The consumed FiniteGaussianSchoenberg.gram_gaussian_posSemidef and the Schur product give finite kernel positivity; closedness gives periodized positivity.

The private kernel_residual_posSemidef subtracts a rank-one kernel while preserving positivity. theta_nonzero proves upper-half-plane theta nonvanishing by duplication and an eventual small-tail bound. It yields strongWave_zero_sum_ne_zero, and hence periodized_kernel_zero_diagonal_pos. A positive diagonal entry excludes zero trace. normalization_isDensity uses GHZMeasureBiseparableBound.IsDensity to complete the density conjunction.

Falsifier

A covariance satisfying the literal uncertainty condition whose exact infinite-sum matrix has a negative quadratic form or zero trace would contradict the statement. Replacing the signed lattice sum, reversing the parity coefficient convention, or asserting convergence from a finite truncation would change the problem. The Lean result uses the exact formulas and infinite sums.

Evidence

The mathematical source is CotfasDVGS.lean, with its Blueprint. The settling GID is D5/S3/Quantum/CotfasDVGS.result; its admission basis is open-problem-resolution (#18946; Proved), generality is I, and utility is none. No fixed-parameter numerical certificate is part of the module. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

The escape audit for D5.S3.Quantum.CotfasDVGS.result is unfinished: #19812. A faithful dependent-family registration lacks a compiled source-reconstruction equivalence bridge, intervention and dependence proofs, and current binding evidence. No Reg mirror or declared_validated registration is delivered.

Declaration classification

The classification expands same-delivery helpers and stops at pinned upstream and existing frozen owners. theta_nonzero supplies the nonvanishing argument on the live path through strongWave_zero_sum_ne_zero and periodized_kernel_zero_diagonal_pos to result. Dependency identities and direct consumers are extracted from compiled proof terms and the scoped Lean report.

Numerical experiment

Experiment directory, commit 04bafcea983207a1fa6056376aa68d57319d2fa1:

• python3 check.py, run from that directory, exits 0. Script SHA-256: e590d9f1a35641dad4b659163e4b678ad34a5857beb62032952007133fa0181b. It checks 600 covariances with $D\ge 1$, including determinant-one samples, at $d\in \{1,3,5,7,9\}$ and $h\in \{0.5,1,3\}$ with lattice cutoff 40: zero failures, worst relative minimum eigenvalue $-7.668186032229494\times 10^{-16}$. All 36 sampled $D<1$ cases are non-PSD.
• python3 identity.py, run from that directory, exits 0. Script SHA-256: 9121d2a4c4a9479e0c28235bce7e4b10dabb256302626e7ac6bf3e29ff48647c. The entrywise kernel-identity error is at most $1.6514567491299204\times 10^{-15}$ for $d\in \{3,5,7\}$ and four covariances.

These are numerical computations on truncated sums, not uniform proofs or a necessity theorem.

Triage

What the settlement shows

Proved, kernel-checked. The nonnegative uncertainty defect controls the Gaussian Gram factor, while a rank-one residual bound and theta nonvanishing give strict diagonal positivity. This handles $D=1$ and $D>1$ in the same argument. The exact normalized matrix is a density operator throughout the source’s stated family.

Explanation from the factorization. At $D=1$, $\lambda =0$ and the Gaussian factor is one; thus the displayed kernel is $g(x)\overline{g(y)}$. The parameter entering the exponential damping is $\pi (D-1)/(2da)$; no equality between $D-1$ alone and a mixing variance is asserted.

Open. Necessity of the uncertainty condition for the discrete matrix, a separate dimension-one theorem, weaker covariance hypotheses, sharpness beyond the source family, and additional coherence results are not settled here. The paper’s uses of these matrices obtain their density-operator premise under the hypotheses of result; no other source theorem is certified by this delivery.

ASSUMED-UNVERIFIED

Literature-search completeness, including the subscription-only Feng–Luo text, remains unverified. No originality of the classical ingredients is claimed. The escape registration remains unfinished under #19812. Finite numerical checks have only the tested scope specified above.