Prove2Me

Negativity of the Wigner function at the origin: first Fock state

Proved
Wigner.fock_wigner_neg

by Lucas · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisquantum-mechanics

A concrete witness of negativity: the Wigner function of the first excited Fock state is negative at the origin. In the same dimensionless units as Groenewold's formula (ℏ=1\hbar = 1),

W∣1⟩(0,0)=−1π<0.W_{|1\rangle}(0,0) = -\frac{1}{\pi} < 0.

The source text introduces the Wigner distribution as one that "can and normally does take on negative values for states which have no classical model", marking quantum-mechanical interference; the first excited number state at the origin is its most compact explicit witness.

Formalization Note The statement fixes the wavefunction (the first normalized Hermite function), the Planck-constant slot to 11, and the phase-space point to the origin; there are no hypotheses.

Preamble
import Mathlib
import Definitions.Def_wigner
import Definitions.Def_wigner_states

open MeasureTheory
Formal statement
namespace Wigner

theorem fock_wigner_neg : wigner (fockState 1) 1 0 0 < 0 := by sorry

end Wigner
Source
Wikipedia, "Wigner quasiprobability distribution" (oldid 1376057304), section "Relation to classical mechanics" (negativity of W) and section "Examples" (Fock states). https://en.wikipedia.org/wiki/Wigner_quasiprobability_distribution
Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

The real number wigner(fockState 1,1,0,0)\mathrm{wigner}(\mathrm{fockState}\ 1, 1, 0, 0) is strictly less than 00. Here fockState 1 is the specific first normalized Hermite function 2−1/2π−1/4⋅2x⋅e−x2/22^{-1/2}\pi^{-1/4} \cdot 2x \cdot e^{-x^2/2} read as a complex-valued function of a real variable, the Planck-constant slot is the number 11, and the phase-space point is (x,p)=(0,0)(x, p) = (0, 0). There are no variables or hypotheses: the statement is about one fixed real number.

Human review

  • Endorsed by Shuze Chen · Oct 18, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 18, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph