Documentation

CsdLean4.CV.Position

CV-1: a finite position observable on a lattice #

Category: 3-Local (a finite position observable on a lattice).

The first constructive step of the continuous-variable track. W4 (CV/ApproxCCR.lean) proved the no-go: no pair of finite matrices satisfies the exact canonical commutation relation [Q, P] = iℏ·1. This module builds the first positive object it motivates — a genuine finite position observable.

On an N-point symmetric grid of spacing a, centered at the origin, the position observable is the diagonal Hermitian matrix

`Q_N = diag(x₀, …, x_{N-1})`,   `x_j = a · (j − (N−1)/2)`,

whose eigenvalues are exactly the N lattice positions (the standard basis vector e_j is an eigenvector with eigenvalue x_j), distinct when a ≠ 0, and bounded by |a|·(N−1)/2. This is a bounded, discrete-spectrum finite observable — precisely the "continuous but limited" observable-value structure the CSD finite-N reading predicts (specs/csd-departures-eft.md §3.1): finitely many levels, evenly spaced, looking continuous for astronomically large N.

CSD reading #

Q_N is an operational position observable in a finite sector. Its spectrum is bounded and discrete — there is a maximum and minimum representable position and finitely many resolvable values — the finite-information-capacity picture, not a spacetime lattice. The continuum position operator is the ideal N → ∞ (with a → 0) limit; at finite N position is this approximate, coarse-grained observable. Conjugate momentum (via the finite Fourier transform) and the approximate CCR ‖[Q_N, P_N] − iℏ·1‖ ≤ ε are the follow-ons CV-2 / CV-3.

Honest scope (load-bearing) #

CV-1 constructs the finite position observable and proves its spectral data (Hermitian, eigenvalues = lattice points, distinct, bounded). It does not construct momentum, does not establish any commutation relation, and does not derive continuous-variable QM. It is the position half of the finite CV sector; momentum and the approximate CCR are CV-2 / CV-3.

Category #

Cat-1: positionOp and its spectral lemmas are CSD-free general facts about a finite diagonal matrix. The CSD interpretation lives only in this docstring.

Main results #

source
noncomputable def CSD.CV.latticePoint (N : ℕ) (a : ℝ) (j : Fin N) :
ℝ

The j-th lattice position on the symmetric N-point grid of spacing a, centered at the origin: x_j = a · (j − (N−1)/2). Real subtraction throughout (no ℕ truncation), so the grid is {−(N−1)/2, …, (N−1)/2} scaled by a.

Equations
Instances For
    source
    noncomputable def CSD.CV.positionOp (N : ℕ) (a : ℝ) :
    Matrix (Fin N) (Fin N) ℂ

    The finite position observable Q_N = diag(x₀, …, x_{N-1}): the diagonal matrix whose entries are the lattice positions.

    Equations
    Instances For
      source
      @[simp]
      theorem CSD.CV.positionOp_apply {N : ℕ} {a : ℝ} (i j : Fin N) :
      positionOp N a i j = if i = j then ↑(latticePoint N a i) else 0
      source
      theorem CSD.CV.positionOp_isHermitian {N : ℕ} {a : ℝ} :
      (positionOp N a).IsHermitian

      Q_N is Hermitian: a genuine self-adjoint observable (real diagonal, so Q_Nᴴ = Q_N), hence has real eigenvalues.

      source
      theorem CSD.CV.positionOp_mulVec_single {N : ℕ} {a : ℝ} (j : Fin N) :
      (positionOp N a).mulVec (Pi.single j 1) = ↑(latticePoint N a j) • Pi.single j 1

      The lattice points are the eigenvalues. The standard basis vector e_j is an eigenvector of Q_N with eigenvalue the lattice position x_j: Q_N · e_j = x_j • e_j. So the standard basis is the position eigenbasis and the spectrum is {x_0, …, x_{N-1}}.

      source
      theorem CSD.CV.latticePoint_injective {N : ℕ} {a : ℝ} (ha : a ≠ 0) :
      Function.Injective (latticePoint N a)

      The eigenvalues are distinct for a ≠ 0: the lattice map j ↦ x_j is injective, so Q_N has N distinct eigenvalues in the N-dimensional space — a non-degenerate observable with N sharp outcomes.

      source
      theorem CSD.CV.abs_latticePoint_le {N : ℕ} {a : ℝ} (j : Fin N) :
      |latticePoint N a j| ≤ |a| * (↑N - 1) / 2

      The spectrum is bounded: every lattice position satisfies |x_j| ≤ |a|·(N−1)/2. So Q_N is a bounded observable with a maximum and minimum representable position — the finite-information-capacity picture.

      source
      theorem CSD.CV.positionOp_trace_eq_zero {N : ℕ} {a : ℝ} :
      (positionOp N a).trace = 0

      The mean position is zero: trace Q_N = 0, since the grid is symmetric about the origin. Proved by the reflection j ↦ Fin.rev j, under which x_{rev j} = −x_j, so the sum equals its own negation.