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: in positive finite dimension and for ℏ ≠ 0, no pair of 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 signed step 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. For N > 0 the grid has extrema; for N = 0 it is empty and the indexed statements are vacuous. This is a bounded, discrete-spectrum finite observable. Equal spacing is a choice of this construction, not a consequence of finite dimension. Approximating a continuous range also requires control of the spacing and span; large N alone does not make the spacing small.

CSD reading

Q_N supplies a finite-sector position model for the interpretation discussed in specs/csd-departures-eft.md §3.1. Its finite spectrum is an observable-value grid; the construction makes no claim about a spacetime lattice. A continuum limit would require embeddings into a common space, a specified notion of convergence, and scaling of both the spacing and span. No such limit is proved here.

CV-2 / CV-3 are implemented separately in CV/Oscillator.lean: its truncated oscillator operators Q and P satisfy QP_commutator and ccr_exact_on_bulk. Those are different operators from this module's positionOp; this file does not construct a Fourier-conjugate momentum or prove a small full-space CCR norm defect.

Honest scope (load-bearing)

CV-1 constructs the finite position observable and proves its spectral data (Hermitian, standard-basis eigenvectors, distinct lattice values when a ≠ 0, and bounded lattice values). 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. The separate oscillator construction cited above supplies the CV-2 / CV-3 results.

Mathematical content

positionOp and its spectral lemmas are CSD-free facts about a finite diagonal matrix. The file is classified as Category 3 by its location in CsdLean4/CV/; the CSD interpretation lives only in this docstring.

Main results

• positionOp_isHermitian : Q_N is Hermitian (a genuine self-adjoint observable).
• positionOp_mulVec_single : Q_N · e_j = x_j • e_j (the lattice points are the eigenvalues, the standard basis is the position eigenbasis).
• latticePoint_injective : the eigenvalues are distinct for a ≠ 0 (N distinct outcomes, a non-degenerate observable).
• abs_latticePoint_le : the spectrum is bounded, |x_j| ≤ |a|·(N−1)/2.
• positionOp_trace_eq_zero : the sum of the lattice eigenvalues is 0. For N > 0, their uniform average is therefore zero; a general state's position expectation need not vanish.

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

The j-th lattice position on the symmetric N-point grid of signed step 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

• CSD.CV.latticePoint N a j = a * (↑↑j - (↑N - 1) / 2)

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

• CSD.CV.positionOp N a = Matrix.diagonal fun (j : Fin N) => ↑(CSD.CV.latticePoint N a j)

@[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

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.

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}}.

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.

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. The index j : Fin N ensures N > 0; in this case the finite grid has maximum and minimum representable positions.

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

The sum of the position eigenvalues is zero: trace Q_N = 0, since the grid is symmetric about the origin. For N > 0, this also gives zero uniform average over the lattice levels, not zero expectation in every state. Proved by the reflection j ↦ Fin.rev j, under which x_{rev j} = −x_j, so the sum equals its own negation.