Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A negative damped spin distribution satisfying the Husimi coefficient bound

Abstract

The damped spin kernel criterion fails for spin three-halves.

Definition 1.1 (Doubled spin selection rules).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.SpinValid (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

The integers j and m are twice the spin and magnetic quantum numbers. The parity condition uses Euclidean integer remainder.

Definition 1.2 (Clebsch–Gordan selection rules).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.CGValid (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

All three magnetic rules, magnetic conservation, the triangle inequalities and total-spin parity are imposed. Variables jone, mone, jtwo and mtwo denote j₁, m₁, j₂ and m₂.

Definition 1.3 (The Condon–Shortley Clebsch–Gordan coefficient).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.CG (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Racah’s factorial formula on doubled integer arguments is zero outside the selection rules. The local fac function is the real cast of the factorial of the nonnegative part of its integer argument. Each live summand has nonnegative factorial arguments. ediv is Lean’s Euclidean integer division; mod is its remainder. The alternating sign is the Condon–Shortley phase.

Definition 1.4 (The ordered spin basis).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.mag (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

The index i in Fin(n+1) labels the basis J, J−1, …, −J, with J=n/2. val is the natural value of a Fin index; castInt is the integer cast.

Definition 1.5 (Irreducible tensors).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.T (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Equation (12), page 2: “the matrix elements of the irreducible tensors in the standard Ĵz-bases are given by ⟨J, m′|T̂^J_{L,k}|J, m⟩ = √((2L + 1)/(2J + 1)) C^{Jm′}{Jm Lk}, where the C^{JM}{j1 m1 j2 m2} denote the Clebsch-Gordan coefficients.” Row i is m′ and column j is m. castReal, castInt and ofReal make the scalar embeddings explicit.

Definition 1.6 (Density-matrix multipoles).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.rhoCoeff (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Equation (13), page 2: “ρ̂ = Σ_{L=0}^{2J} Σ_{k=−L}^{L} ρ_{Lk} T̂^J_{L,k}, ρ_{L,k} = tr((T̂^J_{L,k})† ρ̂).” The adjoint precedes the density matrix in the product.

Definition 1.7 (Legendre polynomials).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.legendre (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Polynomial.shiftedLegendre L is the integer polynomial P_L(1−2x). Mapping to real coefficients and composing with (1−X)/2 gives the ordinary Legendre polynomial for every natural degree.

Definition 1.8 (Associated Legendre functions).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.assocLegendre (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

The Condon–Shortley factor is (−1)^m. iterate(derivative,m,p) means m applications of Polynomial.derivative to p; eval evaluates the resulting polynomial at x. The square root is the nonnegative real square root.

Definition 1.9 (Scaled harmonics of nonnegative order).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.Ypos (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Footnote 1, page 3: “We use the convention Y^0_0 = 1, so that the spherical harmonics are orthonormal with respect to the uniform probability measure dµ^0_{θ,ϕ} = (4π)^{−1} sin θ dθ dϕ. This differs from the Condon–Shortley convention by a factor of √4π: Y^m_L = √4π Y^{m,CS}_L, or equivalently Y^m_L = √(2L+1) Y^{m,Racah}_L, where Y^{m,Racah}_L = (−1)^m √((L−m)!/(L+m)!) P^m_L(cos θ) e^{imϕ} for m ≥ 0.” The usual 1/√4π factor is therefore absent. The imaginary unit is I. Natural subtraction in L−m is expressed by natSub, and factorials have natural arguments.

Definition 1.10 (Scaled harmonics of all integer orders).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.Y (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Nonnegative k uses toNat(k). Negative k uses the Condon–Shortley conjugation identity with natAbs(k). Harmonics vanish outside |k|≤L.

Definition 1.11 (The binomial ratio).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.r (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

The binomial ratio in equations (44) and (53) is a quotient of real casts of natural binomial coefficients.

Definition 1.12 (The damped quasidistribution).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.F (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Equation (44), page 5: “F^σ(θ, ϕ, t) = a_J Σ_{L,k} e^{−γ L(L+1) t/2} ( C(2J, L) / C(2J+L+1, L) )^{−σ/2} ρ_{Lk}(0) overline(Y_{Lk}(θ, ϕ)).” Equations (35)–(36) give a_J=(2J+1)^{−1/2}. The outer sum is over range(n+1) and the inner sum over the integer interval Icc(−castInt(L),castInt(L)). rpow denotes the real power, ofReal the complex embedding. sigma, gamma, theta and phi stand for σ, γ, θ and ϕ.

Definition 1.13 (The positivity conjecture).

Formalization. D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.claim (✓ std3).

Citation. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Section VI, page 8: “For J > 1/2 we do not have an exact result, but it seems reasonable to conjecture that positivity is ensured provided that the damped σ kernel in (44), due to decoherence, becomes no sharper than the Husimi (σ = −1) kernel. That is, if e^{−½γL(L+1)} ( C(2J,L)/C(2J+L+1,L) )^{−σ/2} ≤ ( C(2J,L)/C(2J+L+1,L) )^{1/2} (53) for all L, then we restore positivity.” Equation (12), page 2: “the matrix elements of the irreducible tensors in the standard Ĵz-bases are given by ⟨J, m′|T̂^J_{L,k}|J, m⟩ = √((2L + 1)/(2J + 1)) C^{Jm′}{Jm Lk}, where the C^{JM}{j1 m1 j2 m2} denote the Clebsch-Gordan coefficients.” Equation (13), page 2: “ρ̂ = Σ_{L=0}^{2J} Σ_{k=−L}^{L} ρ_{Lk} T̂^J_{L,k}, ρ_{L,k} = tr((T̂^J_{L,k})† ρ̂).” Equation (44), page 5: “F^σ(θ, ϕ, t) = a_J Σ_{L,k} e^{−γ L(L+1) t/2} ( C(2J, L) / C(2J+L+1, L) )^{−σ/2} ρ_{Lk}(0) overline(Y_{Lk}(θ, ϕ)).” Footnote 1, page 3: “We use the convention Y^0_0 = 1, so that the spherical harmonics are orthonormal with respect to the uniform probability measure dµ^0_{θ,ϕ} = (4π)^{−1} sin θ dθ dϕ. This differs from the Condon–Shortley convention by a factor of √4π: Y^m_L = √4π Y^{m,CS}_L, or equivalently Y^m_L = √(2L+1) Y^{m,Racah}_L, where Y^{m,Racah}_L = (−1)^m √((L−m)!/(L+m)!) P^m_L(cos θ) e^{imϕ} for m ≥ 0.” The encoding uses n=2J≥2, sigma∈[−1,1], gamma>0, t≥0, every L≤n, every positive semidefinite unit-trace matrix rho on Fin(n+1), and all real angles theta and phi. IsDensity is the existing positive-semidefinite unit-trace predicate. Equation (53) is printed without t; the time-dependent premise follows (44), and the counterexample has t=1 so both readings coincide. Real-part nonnegativity is a necessary condition for positivity. The symbols X and I in the definitions denote Polynomial.X and Complex.I, respectively.

Theorem 1.14 (Refutation at spin three-halves).

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.result (✓ std3). ∎

Resolves. Problems/brody-graefe-melanathuru-2026-damped-kernel-positivity (refuted) by D5/S3/Quantum/Decoherence/DampedSpinKernelPositivityRefutation.result.

Source. Repository-derived.

Acknowledgement. Dorje C. Brody; Eva-Maria Graefe; Rishindra Melanathuru (2026). Phase-space measurements and decoherence for angular momentum systems. DOI: 10.48550/arXiv.2605.02696. URL: https://arxiv.org/abs/2605.02696v1.

Commentary.

Set n=3, sigma=1, gamma=log(20/11), t=1, rho=Matrix.single(3,3,1) on Fin 4, and theta=phi=0. The four binomial ratios are 1, 3/5, 1/5 and 1/35, and q=exp(−gamma)=11/20 satisfies q^(L(L+1)/2)≤r(3,L) for every L≤3. At the north pole only k=0 contributes. The lowest-weight state’s multipole signs alternate, giving F=(1−3q+5q³−7q⁶)/4=−760927/256000000<0. The density predicate is reused directly from D5/S3/QuantumChannels/CoPRelativeQuantumnessRefutation.IsDensity: positive semidefinite and trace one. The counterexample has t=1, so equation (53)’s printed omission of t does not affect the refutation.

References