Consequences of the Weyl relations

Proved

QAlgorithms.Papers.Independent.Intake100.P23.weylRelations_consequences

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $Y$ be a real vector space with antisymmetric real bilinear form $\omega$ , possibly degenerate. Let $W:Y\to\mathcal U(H)$ be a Weyl representation on any complex Hilbert space, so $W(y)W(z)=e^{-i\omega(y,z)/2}W(y+z)$ . Then

\begin{gathered}W(y)W(z)=e^{-i\omega(y,z)}W(z)W(y),\\W(y)^*=W(-y),\quad W(0)=1,\\W(sy)W(ty)=W((s+t)y)\quad(s,t\in\mathbb R).\end{gathered}

These identities supply inverses and the one-parameter groups underlying field operators.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P23

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intake100.P23

open QAlgorithms.Papers.Independent.Renew46.P03 (tensorVector)

variable {Y : Type*} [AddCommGroup Y] [Module ℝ Y]

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

/-- PDF p.9, Theorem 2: all of (10), (11), and (12). -/
theorem weylRelations_consequences (omega : Y →ₗ[ℝ] Y →ₗ[ℝ] ℝ)
    (hanti : Antisymmetric omega) (W : Y → H →L[ℂ] H) (hW : IsCCR omega W) :
    (∀ y z, W y * W z = Complex.exp (-Complex.I * (omega y z : ℂ)) • (W z * W y)) ∧
    (∀ y, star (W y) = W (-y)) ∧ W 0 = 1 ∧
    (∀ (y : Y) (s t : ℝ), W (s • y) * W (t • y) = W ((s + t) • y)) := by sorry

end QAlgorithms.Papers.Independent.Intake100.P23

end

Source

Introduction to representations of the canonical commutation and anticommutation relations, arXiv:math-ph/0511030v2, PDF p. 9, Theorem 2

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $Y$ be a real vector space, $H$ a complex Hilbert space, $\omega:Y\times Y\to\mathbb R$ a real bilinear form satisfying $\omega(y,z)=-\omega(z,y)$ for all $y,z$ , and $W:Y\to\mathcal B(H)$ a family of bounded complex-linear operators. Suppose every $W(y)$ is unitary and $W(y)W(z)=e^{-i\omega(y,z)/2}W(y+z)$ for all $y,z\in Y$ . Then $W(y)W(z)=e^{-i\omega(y,z)}W(z)W(y)$ for all $y,z$ ; $W(y)^*=W(-y)$ for every $y$ ; $W(0)=I_H$ ; and $W(sy)W(ty)=W((s+t)y)$ for every $y\in Y$ and every $s,t\in\mathbb R$ . No regularity, irreducibility, or nondegeneracy assumption is imposed, and zero spaces are included.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph