CV-2 / CV-3: the truncated oscillator and the approximate CCR

Category: 3-Local (the truncated oscillator and the approximate CCR).

W4 (CV/ApproxCCR.lean) proved that no finite matrices satisfy the exact canonical commutation relation [Q, P] = iℏ·1 — the trace of a commutator is 0, the trace of iℏ·1 is iℏN ≠ 0. CV-1 (CV/Position.lean) built a finite position observable. This module builds the conjugate (Q, P) pair and the sharp approximate CCR: the relation [Q, P] = iℏ·1 holds exactly on a low-energy sector, failing only by a rank-one defect at the top level — and it must fail there, by exactly the amount that makes the trace vanish (W4).

The construction is the N-level truncated harmonic oscillator. With the annihilation operator a (a·eₙ = √n·e_{n-1}) and creation a† = aᴴ:

• creation_mul_annihilation : a†a = diag(0,1,…,N−1) — the number operator;
• annihilation_mul_creation : aa† = diag(1,2,…,N−1,0);
• truncated_ccr : [a, a†] = 1 − N·|N−1⟩⟨N−1| — the CCR with a rank-one defect at the top Fock level, the finite trace of both sides being 0 (W4).

Then Q = (a + a†)/√2, P = (a − a†)/(i√2) are Hermitian, and:

• QP_commutator : [Q, P] = i·[a, a†];
• ccr_exact_on_bulk : [Q, P]·eₙ = i·eₙ for every n ≠ N−1 — the exact CCR on the low-energy sector (all Fock levels but the top).

So the additive CCR is available approximately: exact away from the boundary, with the unavoidable defect (W4) pushed entirely into the highest level. On states with negligible top-level population the defect is negligible, i.e. ‖[Q, P] − i·1‖ is small on the low-energy sector.

CSD reading

A finite operational sector realises position and momentum as an approximately canonical pair: the commutator is i·1 throughout the bulk and departs from it only at the sector's energy ceiling — the finite-information-capacity boundary. The continuum CCR is the N → ∞ limit in which the boundary recedes to infinity.

Honest scope (load-bearing)

This constructs one concrete conjugate pair and proves its commutator exactly. It does not derive continuous-variable QM and does not claim the oscillator is canonical (W4 forbids that in finite dimension); the boundary defect is displayed honestly, not hidden.

Category

Cat-1: annihilation, creation, Q, P and all lemmas are CSD-free general facts about finite complex matrices. The CSD interpretation lives only in the docstrings.

Two index-sum helpers

theorem CSD.CV.sum_ite_valEq (N c : ℕ) (v : ℂ) : (∑ j : Fin N, if ↑j = c then v else 0) = if c < N then v else 0

A single-term sum: ∑_{j:Fin N} [j = c]·v = [c < N]·v.

theorem CSD.CV.sum_ite_valAdd (N c : ℕ) (v : ℂ) : (∑ j : Fin N, if ↑j + 1 = c then v else 0) = if 1 ≤ c ∧ c ≤ N then v else 0

A single-term sum for the shifted condition: ∑_{j:Fin N} [j+1 = c]·v = [1 ≤ c ∧ c ≤ N]·v`.

theorem CSD.CV.sqrt_mul_self_cast (n : ℕ) : ↑√↑n * ↑√↑n = ↑n

(√n : ℂ)·(√n : ℂ) = n.

The ladder operators

noncomputable def CSD.CV.annihilation (N : ℕ) : Matrix (Fin N) (Fin N) ℂ

The annihilation operator on the N-level truncated oscillator: a·eₙ = √n·e_{n-1} (and a·e₀ = 0). As a matrix, a_{ij} = √j when i + 1 = j, else 0 (one super-diagonal of square roots).

Equations

• CSD.CV.annihilation N = Matrix.of fun (i j : Fin N) => if ↑i + 1 = ↑j then ↑√↑↑j else 0

noncomputable def CSD.CV.creation (N : ℕ) : Matrix (Fin N) (Fin N) ℂ

The creation operator a† = aᴴ: a†·eₙ = √(n+1)·e_{n+1} (and a†·e_{N-1} = 0, the truncation).

Equations

• CSD.CV.creation N = (CSD.CV.annihilation N).conjTranspose

noncomputable def CSD.CV.numberOp (N : ℕ) : Matrix (Fin N) (Fin N) ℂ

The number operator N̂ = diag(0, 1, …, N−1).

Equations

• CSD.CV.numberOp N = Matrix.diagonal fun (i : Fin N) => ↑↑i

noncomputable def CSD.CV.topProj (N : ℕ) : Matrix (Fin N) (Fin N) ℂ

The top-level projector |N−1⟩⟨N−1| = diag(0, …, 0, 1), where the CCR defect lives.

Equations

• CSD.CV.topProj N = Matrix.diagonal fun (i : Fin N) => if ↑i = N - 1 then 1 else 0

@[simp]

theorem CSD.CV.annihilation_apply {N : ℕ} (i j : Fin N) : annihilation N i j = if ↑i + 1 = ↑j then ↑√↑↑j else 0

@[simp]

theorem CSD.CV.creation_apply {N : ℕ} (i j : Fin N) : creation N i j = if ↑j + 1 = ↑i then ↑√↑↑i else 0

The two products

theorem CSD.CV.creation_mul_annihilation {N : ℕ} : creation N * annihilation N = numberOp N

a†a = N̂: creation ∘ annihilation is the number operator diag(n).

theorem CSD.CV.annihilation_mul_creation {N : ℕ} : annihilation N * creation N = Matrix.diagonal fun (i : Fin N) => if ↑i + 1 < N then ↑(↑i + 1) else 0

aa† = diag(1, 2, …, N−1, 0): annihilation ∘ creation, the number operator shifted up by one with a zero at the top level.

The truncated CCR

theorem CSD.CV.truncated_ccr {N : ℕ} : annihilation N * creation N - creation N * annihilation N = 1 - ↑N • topProj N

The truncated CCR: [a, a†] = 1 − N·|N−1⟩⟨N−1|. The canonical commutation relation holds everywhere except a rank-one defect at the top Fock level. Both sides have trace 0 (W4): tr 1 = N and tr(N·|N−1⟩⟨N−1|) = N.

The conjugate pair Q, P and the approximate CCR

noncomputable def CSD.CV.Q (N : ℕ) : Matrix (Fin N) (Fin N) ℂ

The position quadrature Q = (a + a†)/√2.

Equations

• CSD.CV.Q N = (↑√2)⁻¹ • (CSD.CV.annihilation N + CSD.CV.creation N)

noncomputable def CSD.CV.P (N : ℕ) : Matrix (Fin N) (Fin N) ℂ

The momentum quadrature P = (a − a†)/(i√2) = (−i/√2)·(a − a†).

Equations

• CSD.CV.P N = (-Complex.I * (↑√2)⁻¹) • (CSD.CV.annihilation N - CSD.CV.creation N)

theorem CSD.CV.sqrt2_mul_sqrt2 : ↑√2 * ↑√2 = 2

√2·√2 = 2 in ℂ.

theorem CSD.CV.sqrt2_ne_zero : ↑√2 ≠ 0

√2 ≠ 0 in ℂ.

theorem CSD.CV.Q_isHermitian {N : ℕ} : (Q N).IsHermitian

Q is Hermitian (a genuine self-adjoint observable).

theorem CSD.CV.P_isHermitian {N : ℕ} : (P N).IsHermitian

P is Hermitian (a genuine self-adjoint observable).

theorem CSD.CV.QP_commutator {N : ℕ} : Q N * P N - P N * Q N = Complex.I • (annihilation N * creation N - creation N * annihilation N)

[Q, P] = i·[a, a†]: the quadrature commutator is i times the ladder commutator.

theorem CSD.CV.ccr_exact_on_bulk {N : ℕ} (j : Fin N) (hj : ↑j ≠ N - 1) : (Q N * P N - P N * Q N).mulVec (Pi.single j 1) = Complex.I • Pi.single j 1

The exact CCR on the low-energy sector. For every Fock state below the top level (n ≠ N−1), the quadratures satisfy the canonical commutation relation exactly: [Q, P]·eₙ = i·eₙ. The defect (W4-forced) is confined to the top level, so on any state with negligible top-level population ‖[Q,P] − i·1‖ is negligible.