slug: de-boer-di-giulio-keski-vakkuri-tonni-2024-wigner-majorization-chains
bibkey: deboer2025wignermajorization
doi: 10.1103/w561-h3z5
url: https://arxiv.org/abs/2412.19698v3
triage: theorem
motivation_gids:
  - D5/S3/Quantum/QuantumChannels/FockAttenuator/VacuumOnePhotonWignerMajorization.result

Vacuum and one-photon Wigner-majorization chains

Problem

De Boer, Di Giulio, Keski-Vakkuri and Tonni, Continuous majorization in quantum phase space for Wigner-positive states and proposals for Wigner-negative states, arXiv:2412.19698v3, Section V.A.1, ask for an analytic understanding of ordered subsets of the vacuum/one-photon mixture family. The v1 question is: “It would be interesting to identify subsets of W̃_u in which all elements exhibit a Wigner majorization relationship with one another. We leave this question for future works.” The v3 conjecture concerns the branch above one half. Preregistration #18571 specifies DBKT-1: both closed intervals form chains under Proposal 1.

Statement echo

Definitions of the functions are meaningful for every real parameter; the theorem imposes the source’s physical parameter intervals. Endpoints and all nonnegative thresholds are included. No clause is dropped.

Motivation

D5/S3/Quantum/QuantumChannels/FockAttenuator/VacuumOnePhotonWignerMajorization.result proves the two chain assertions. D5/S3/Analytic/Convexity/DerivativeHingeMajorization supplies the general analytic statements. Its cancellation theorem treats continuous profiles with an everywhere derivative, an integrable derivative, one nonnegative peak position, the corresponding derivative signs, and zero endpoint values at zero and infinity.

Gap

The paper’s numerical chain on the Wigner-negative branch supplies individual comparisons. The universal statement requires every ordered pair on each branch and every nonnegative threshold. The vacuum-majorization theorem for Wigner-positive mixtures of the lowest three Fock states supplies a different endpoint comparison; it does not state either complete chain.

Route

With $s=x^2+p^2$, $h(s)=s{e}^{-s}$, $k(s)=(1-s)e^{-s}$ and $c=1-2u$, the mixture satisfies $\pi {\tilde{W}}_u=h+ck$. mixture_closed and level_reduction identify its level functional with $J_T(c)={\int }_0^{\infty }\max (|h+ck|-T,0)ds$, where $T=\pi t$. The general radial identity supplies the polar factor. boundary_cancellation gives $\int k{1}_{h>T}=0$; concrete_cancel applies it to this profile. hinge_min integrates a supporting-line inequality, while hinge_convex establishes convexity. convex_rays and concrete_rays give the opposite monotonicities on the rays meeting at $c=0$. result transfers them to the two parameter intervals.

Falsifier

An ordered pair in either stated interval and a nonnegative threshold violating its inequality would refute DBKT-1. A failure of the source correspondence, integrability, cancellation, or the convex minimum would invalidate the proposed route. Strict inequalities and comparisons between the branches are separate assertions.

Evidence

The canonical source is D5/S3/Quantum/QuantumChannels/FockAttenuator/VacuumOnePhotonWignerMajorization.lean, supported by D5/S3/Analytic/Convexity/DerivativeHingeMajorization.lean. Their Scribes display every public definition and theorem, including the expanded proposition of result. The source locator and literature scope are in Library/ContinuousObservables/deboer2025wignermajorization.md.

The four-slot escape audit is unfinished: #20140. Its targets are radial, boundary_cancellation, hinge_min, hinge_convex, convex_rays, and the settling result. A faithful compiled realization and readout for the full analytic telescopes is missing; no declared_validated registration is claimed.

Experiment

Independent numerical checks use the pinned check.py, SHA-256 26165b657205c4f6d509c5a79fbaa3a07a13ecab3c2a79a61cbe378b33b5cfd8. Command: python3 /Users/auric/trureturing-experiments/docs/reports/deboer-digiulio-keskivakkuri-tonni-2025-vacuum-one-photon-wigner-majorization/check.py, exit 0. Each branch has 8610 pair/threshold comparisons: parameters on the $1/40$ grid and 41 thresholds in $[0,1/\pi ]$, with zero violations. The maximum closed-form error for $I_0$ and $M$ is $7.1491\cdot 10^{-30}$. The checker finds opposite signs of level-functional differences at tested thresholds for all 190 tested cross-branch pairs $0<u<1/2<v\le 1-u$. The five specified plane quadratures on $[-7,7{]}^2$ differ from radial values by less than $2\cdot 10^{-7}$. The full-family and reversed-direction controls have their expected outcomes. These are finite numerical readings, not universal proofs.

Triage

Tier 1: an explicit published question and conjecture, with settlement Proved under #18571. The literature reading checks source versions v1 and v3, Van Herstraeten–Jabbour–Cerf (Quantum 7, 1021), Upadhyaya et al. arXiv:2507.22986v2, the citing works and repository scope described in the preregistration. Completeness is ASSUMED-UNVERIFIED.

What the settlement shows

The decisive mechanism is the common minimum of every level functional at $u=1/2$, obtained by cancellation of the derivative direction over superlevel sets. The general lemmas allow other continuous nonnegative profiles when their derivative, integrability, sign and endpoint hypotheses are supplied. They do not assert strictness. The two chains identify mutually comparable subsets requested in v1 and include the v3 conjectured branch. They do not alter Proposal 1 or establish any claim for the paper’s other preorders.

Declaration classification

Classification expands both delivered modules and stops at protected-base owners and pinned Mathlib. The dependency edges and their propagation are computed from compiled proof terms; the normalization/content boundary is a semantic judgement. The equality from boundary_cancellation remains on the live proof path of both ray components and of the settling result. The tables identify the source declarations, omitting compiler-generated auxiliaries.

ASSUMED-UNVERIFIED

Literature-screen completeness and any claim of originality beyond the searched scope are unverified. The published question and the exact chain proposition are distinct from empirical physical claims. Four-slot registration remains unfinished under #20140. Strictness, complete cross-branch classification and the general non-unimodal absolutely continuous extension remain open.