CV-28: Wick's theorem at the cutoff — every word, every time

Category: 3-Local (CV; continuous variables — the multi-mode field).

CV-23 proved Wick's theorem at the cutoff for four quadratures at distinct stroboscopic periods (timeFourPoint_wick) and, in CV-23d, for an arbitrary equal-time word (wordOp_vac_eq_prod_wickMoment). This module states it once, for every word and every real time: the vacuum expectation of Q_{k₁}(t₁) ⋯ Q_{kₘ}(tₘ), each quadrature at its own Heisenberg time under the free field, is the sum over perfect matchings of the insertions of the product of the propagator lines, a line joining two insertions of the same mode with the kernel ½ e^{−i tᵢ} e^{+i tⱼ}. The pairing sum is written in its first-contraction recursive form (wickSum): the leftmost insertion is contracted with each later insertion of its mode in turn, and the rest is the pairing sum of the word with the two removed.

• quadratureAt t — the single-mode quadrature at time t, e^{−it}/√2 · a + e^{it}/√2 · a† (quadratureAt_apply: the free phases dress the two hops); timeQ t k — the quadrature of mode k at real time t, U(t)† Q_k U(t), and ★ timeQ_eq_modeOp — it is modeOp k of quadratureAt t;
• timeWord l — the product of the insertions (k, t) of a word, in the written order; contraction x y — the propagator line, δ_{kl} · ½ e^{−it} e^{+is}; wickSum l — the pairing sum, wickSum [] = 1, wickSum (x :: l) = ∑ⱼ contraction x lⱼ · wickSum (l without j);
• ★★ timeWord_vac_eq_wickSum — Wick's theorem at the cutoff, every word, every time: below the threshold count k / 2 < N for every mode, ⟨vac∣ Q_{k₁}(t₁) ⋯ Q_{kₘ}(tₘ) ∣vac⟩ = wickSum [(k₁, t₁), …, (kₘ, tₘ)]. The proof is the first-contraction recursion ★ timeWord_cons_vac: the vacuum row of the leftmost quadrature is its annihilator row; commuting the annihilator through the rest of the word (mul_map_prod_sub_map_prod_mul, the commutator of a product one factor at a time) meets the truncated CCR at each later insertion of the same mode (annihilation_quadratureAt_commutator); the CCR's rank-one defect at the top level dies because the word cannot lift the vacuum that high on both sides of the defect at once (timeWord_apply_eq_zero_of_lt, the walk band, and timeWord_mul_topProj_mul_timeWord_vac);
• corollaries — wickSum_eq_zero_of_odd (odd words vanish), wickSum_pair, wickSum_four (the three pairings), ★ timeFourPoint_eq_wickSum (CV-23b's four-point function is the pairing sum at stroboscopic times: contraction_natMul is twoPointKernel), ★ wickSum_map_zero (at equal time the pairing sum is CV-23d's ∏_k wickMoment (count k)), and ★★ dysonTerm_two_vac_wordOp — the second-order vacuum diagrams of every monomial vertex: for V = Q_{k₁} ⋯ Q_{kₘ} the two-vertex amplitude of CV-27 is the ordered double integral of the pairing sum of the word with itself at the time difference — the Q⁴ sunset and its disconnected partners, at the cutoff, as a theorem;
• ★★ wickSum_eq_pairingSum / ★★ timeWord_vac_eq_pairingSum — the matching-indexed form: wickSum l is Fin.pairingSum of the contraction on the positions of l, the sum over perfect matchings σ of Fin m of ∏_{i < σ i} contraction lᵢ l_{σ i}; so the vacuum expectation of a word is the sum over the perfect matchings of its insertions of the product of the propagator lines, Wick's theorem as the textbook states it.

Why the threshold. Contracting the leftmost insertion of mode k with a later one leaves the CCR defect N · |N−1⟩⟨N−1| sandwiched between the two halves of the word; a half with fewer than N − 1 insertions of mode k cannot connect the vacuum to the top level, and with count k < 2N one half always has fewer. Exactly CV-23c's n < N, one insertion at a time.

Honest scope

⚠️ Two forms of the pairing sum. wickSum is the pairing sum computed by first contraction; ★★ wickSum_eq_pairingSum identifies it with the matching-indexed form of Mathlib/Combinatorics/PairingSum.lean — the sum over fixed-point-free involutions σ of the positions of the product over the pairs i < σ i of contraction lᵢ l_{σ i} — and ★★ timeWord_vac_eq_pairingSum states Wick's theorem in that textbook form.

⚠️ Finite cutoff, free dynamics. The thresholds are where Wick survives truncation; the times are Heisenberg times under the free field only. Nothing continuum is claimed.

References: CV/Wick.lean (CV-23b/c: timeFourPoint_wick, twoPointKernel, the walk band and the moment recursion this module generalises); CV/WickGeneral.lean (CV-23d); CV/FeynmanVertex.lean (CV-27, dysonTerm_two_vac); CV/Oscillator.lean (truncated_ccr, topProj); CV/ModeLocality.lean (modeOp, commute_modeOp); Mathlib/Combinatorics/PairingSum.lean (Fin.pairingSum, Fin.pairingSum_succ_succ); specs/BACKLOG.md #36(b)(iv), (iv′); specs/future-work.md (row CV-28).

A commutator through a product

theorem CSD.CV.mul_map_prod_sub_map_prod_mul {R : Type u_1} {α : Type u_2} [Ring R] (A : R) (f : α → R) (l : List α) : A * (List.map f l).prod - (List.map f l).prod * A = ∑ j : Fin l.length, (List.map f (List.take (↑j) l)).prod * (A * f l[j] - f l[j] * A) * (List.map f (List.drop (↑j + 1) l)).prod

The commutator with a product, one factor at a time: [A, ∏ f l] = ∑ⱼ (∏ f (l.take j)) · [A, f lⱼ] · (∏ f (l.drop (j + 1))).

The single-mode quadrature at time t

noncomputable def CSD.CV.ladderPhase (t : ℝ) : ℂ

The coefficient e^{−it}/√2 of the annihilator in the evolved quadrature.

Equations

• CSD.CV.ladderPhase t = (↑√2)⁻¹ * Complex.exp (-(Complex.I * ↑t))

theorem CSD.CV.ladderPhase_mul_ladderPhase_neg (t s : ℝ) : ladderPhase t * ladderPhase (-s) = 2⁻¹ * Complex.exp (-(Complex.I * ↑t)) * Complex.exp (Complex.I * ↑s)

noncomputable def CSD.CV.quadratureAt {N : ℕ} (t : ℝ) : Matrix (Fin N) (Fin N) ℂ

The single-mode quadrature at time t: Q(t) = e^{−it}/√2 · a + e^{it}/√2 · a†.

Equations

• CSD.CV.quadratureAt t = CSD.CV.ladderPhase t • CSD.CV.annihilation N + CSD.CV.ladderPhase (-t) • CSD.CV.creation N

theorem CSD.CV.quadratureAt_apply {N : ℕ} (t : ℝ) (i j : Fin N) : quadratureAt t i j = Complex.exp (Complex.I * ↑t * (↑↑i - ↑↑j)) * Q N i j

The free phases dress the two hops: Q(t) i j = e^{it (i − j)} · Q i j.

theorem CSD.CV.quadratureAt_apply_eq_zero_of_far {N : ℕ} [NeZero N] (t : ℝ) {i j : Fin N} (h1 : ↑i + 1 ≠ ↑j) (h2 : ↑j + 1 ≠ ↑i) : quadratureAt t i j = 0

The evolved quadrature is strictly tridiagonal, like the bare one.

theorem CSD.CV.annihilation_quadratureAt_commutator {N : ℕ} (t : ℝ) : annihilation N * quadratureAt t - quadratureAt t * annihilation N = ladderPhase (-t) • (1 - ↑N • topProj N)

The truncated CCR against the evolved quadrature: [a, Q(t)] = e^{it}/√2 · (1 − N · topProj).

modeOp algebra

theorem CSD.CV.modeOp_apply_of_not_agree {K N : ℕ} (k : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) {c d : FieldConfig K N} (h : ¬∀ (j : Fin K), j ≠ k → c j = d j) : modeOp k a c d = 0

theorem CSD.CV.modeOp_add {K N : ℕ} (k : Fin K) (a b : Matrix (Fin N) (Fin N) ℂ) : modeOp k (a + b) = modeOp k a + modeOp k b

theorem CSD.CV.modeOp_smul {K N : ℕ} (k : Fin K) (r : ℂ) (a : Matrix (Fin N) (Fin N) ℂ) : modeOp k (r • a) = r • modeOp k a

theorem CSD.CV.modeOp_sub {K N : ℕ} (k : Fin K) (a b : Matrix (Fin N) (Fin N) ℂ) : modeOp k (a - b) = modeOp k a - modeOp k b

theorem CSD.CV.modeOp_diagonal {K N : ℕ} (k : Fin K) (f : Fin N → ℂ) : modeOp k (Matrix.diagonal f) = Matrix.diagonal fun (c : FieldConfig K N) => f (c k)

modeOp of a diagonal matrix is diagonal in the configuration basis.

theorem CSD.CV.modeOp_creation_vac_apply {K N : ℕ} [NeZero N] (k : Fin K) (e : FieldConfig K N) : modeOp k (creation N) (vacCfg K N) e = 0

The creation operator has no vacuum row.

theorem CSD.CV.modeOp_annihilation_apply_vac {K N : ℕ} [NeZero N] (k : Fin K) (e : FieldConfig K N) : modeOp k (annihilation N) e (vacCfg K N) = 0

The annihilation operator has no vacuum column.

The quadrature of a mode at a real time

theorem CSD.CV.heisenberg_freeFieldU_apply {K N : ℕ} (τ : ℝ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (c d : FieldConfig K N) : heisenberg (freeFieldU K N τ) A c d = Complex.exp (Complex.I * ↑τ * (↑(fieldEnergy c) - ↑(fieldEnergy d))) * A c d

The Heisenberg entry formula for the free evolution at a real time.

theorem CSD.CV.fieldEnergy_sub_of_agree {K N : ℕ} {c d : FieldConfig K N} (k : Fin K) (h : ∀ (j : Fin K), j ≠ k → c j = d j) : fieldEnergy c - fieldEnergy d = ↑↑(c k) - ↑↑(d k)

Configurations agreeing off one mode differ in energy by that mode's occupation.

noncomputable def CSD.CV.timeQ {K N : ℕ} (t : ℝ) (k : Fin K) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The quadrature of mode k at real time t: Q_k(t) = U(t)† Q_k U(t).

Equations

• CSD.CV.timeQ t k = CSD.CV.heisenberg (CSD.CV.freeFieldU K N t) (CSD.CV.modeOp k (CSD.CV.Q N))

theorem CSD.CV.timeQ_eq_modeOp {K N : ℕ} (t : ℝ) (k : Fin K) : timeQ t k = modeOp k (quadratureAt t)

★ The evolved mode quadrature is the single-mode evolved quadrature on its mode.

theorem CSD.CV.timeQ_support {K N : ℕ} [NeZero N] (t : ℝ) (k : Fin K) {c d : FieldConfig K N} (h : timeQ t k c d ≠ 0) : (∀ (j : Fin K), j ≠ k → c j = d j) ∧ (↑(c k) + 1 = ↑(d k) ∨ ↑(d k) + 1 = ↑(c k))

Where an evolved quadrature has an entry: the configurations agree off its mode and differ by one quantum on it.

theorem CSD.CV.modeOp_annihilation_timeQ_commutator {K N : ℕ} (t : ℝ) (k k' : Fin K) : modeOp k (annihilation N) * timeQ t k' - timeQ t k' * modeOp k (annihilation N) = if k' = k then ladderPhase (-t) • (1 - ↑N • modeOp k (topProj N)) else 0

The commutator of a mode's annihilator with an evolved quadrature: zero at another mode, the truncated CCR at its own.

Words at their times, the contraction and the pairing sum

noncomputable def CSD.CV.timeWord {K N : ℕ} (l : List (Fin K × ℝ)) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The word Q_{k₁}(t₁) ⋯ Q_{kₘ}(tₘ) of the insertions (kᵢ, tᵢ), in the written order.

Equations

• CSD.CV.timeWord l = (List.map (fun (x : Fin K × ℝ) => CSD.CV.timeQ x.2 x.1) l).prod

@[simp]

theorem CSD.CV.timeWord_nil {K N : ℕ} : timeWord [] = 1

theorem CSD.CV.timeWord_cons {K N : ℕ} (x : Fin K × ℝ) (l : List (Fin K × ℝ)) : timeWord (x :: l) = timeQ x.2 x.1 * timeWord l

theorem CSD.CV.timeWord_append {K N : ℕ} (l₁ l₂ : List (Fin K × ℝ)) : timeWord (l₁ ++ l₂) = timeWord l₁ * timeWord l₂

theorem CSD.CV.timeWord_eraseIdx {K N : ℕ} (l : List (Fin K × ℝ)) (j : ℕ) : timeWord (l.eraseIdx j) = timeWord (List.take j l) * timeWord (List.drop (j + 1) l)

noncomputable def CSD.CV.contraction {K : ℕ} (x y : Fin K × ℝ) : ℂ

The contraction (propagator line) of two insertions: δ_{kl} · ½ e^{−it} e^{+is}.

Equations

• CSD.CV.contraction x y = if x.1 = y.1 then 2⁻¹ * Complex.exp (-(Complex.I * ↑x.2)) * Complex.exp (Complex.I * ↑y.2) else 0

@[irreducible]

noncomputable def CSD.CV.wickSum {K : ℕ} : List (Fin K × ℝ) → ℂ

The pairing sum, in first-contraction form: the leftmost insertion is contracted with each later one in turn, and the rest is the pairing sum of the word with the two removed.

Equations

• CSD.CV.wickSum [] = 1
• CSD.CV.wickSum (x_1 :: l) = ∑ j : Fin l.length, CSD.CV.contraction x_1 l[j] * CSD.CV.wickSum (l.eraseIdx ↑j)

@[simp]

theorem CSD.CV.wickSum_nil {K : ℕ} : wickSum [] = 1

theorem CSD.CV.wickSum_cons {K : ℕ} (x : Fin K × ℝ) (l : List (Fin K × ℝ)) : wickSum (x :: l) = ∑ j : Fin l.length, contraction x l[j] * wickSum (l.eraseIdx ↑j)

The walk band

theorem CSD.CV.timeWord_apply_eq_zero_of_lt {K N : ℕ} [NeZero N] (l : List (Fin K × ℝ)) (c d : FieldConfig K N) (k : Fin K) : ↑(c k) + List.count k (List.map Prod.fst l) < ↑(d k) → timeWord l c d = 0

The walk band, row form: a word cannot raise a mode by more than its number of insertions of that mode.

theorem CSD.CV.timeWord_apply_eq_zero_of_lt' {K N : ℕ} [NeZero N] (l : List (Fin K × ℝ)) (c d : FieldConfig K N) (k : Fin K) : ↑(d k) + List.count k (List.map Prod.fst l) < ↑(c k) → timeWord l c d = 0

The walk band, column form: a word cannot lower a mode by more than its number of insertions of that mode.

theorem CSD.CV.timeWord_mul_topProj_mul_timeWord_vac {K N : ℕ} [NeZero N] (l₁ l₂ : List (Fin K × ℝ)) (k : Fin K) (h : List.count k (List.map Prod.fst l₁) + List.count k (List.map Prod.fst l₂) + 2 < 2 * N) : (timeWord l₁ * modeOp k (topProj N) * timeWord l₂) (vacCfg K N) (vacCfg K N) = 0

The defect dies below threshold: with fewer than 2N − 2 insertions of mode k in the two halves together, the top-level projector of mode k sandwiched between them has no vacuum expectation — one half cannot reach the top level.

The first-contraction recursion

theorem CSD.CV.count_map_fst_eq {K : ℕ} (l : List (Fin K × ℝ)) (j : Fin l.length) (k : Fin K) : List.count k (List.map Prod.fst l) = (List.count k (List.map Prod.fst (List.take (↑j) l)) + if l[j].1 = k then 1 else 0) + List.count k (List.map Prod.fst (List.drop (↑j + 1) l))

The count of a mode in a word, split at an insertion.

theorem CSD.CV.timeWord_cons_vac {K N : ℕ} [NeZero N] (x : Fin K × ℝ) (l : List (Fin K × ℝ)) (hN : ∀ (k : Fin K), List.count k (List.map Prod.fst (x :: l)) < 2 * N) : timeWord (x :: l) (vacCfg K N) (vacCfg K N) = ∑ j : Fin l.length, contraction x l[j] * timeWord (l.eraseIdx ↑j) (vacCfg K N) (vacCfg K N)

★ The first-contraction recursion: below threshold, the vacuum expectation of a word is the sum over the later insertions of the contraction of the leftmost with it, times the vacuum expectation of the word with the two removed.

Wick's theorem, every word, every time

theorem CSD.CV.timeWord_vac_eq_wickSum {K N : ℕ} [NeZero N] (l : List (Fin K × ℝ)) : (∀ (k : Fin K), List.count k (List.map Prod.fst l) < 2 * N) → timeWord l (vacCfg K N) (vacCfg K N) = wickSum l

★★ Wick's theorem at the cutoff, for every word at every time. Below the threshold count k < 2N for every mode, the vacuum expectation of Q_{k₁}(t₁) ⋯ Q_{kₘ}(tₘ) is the pairing sum wickSum [(k₁, t₁), …, (kₘ, tₘ)].

theorem CSD.CV.timeWord_vac_eq_wickSum' {K N : ℕ} [NeZero N] (l : List (Fin K × ℝ)) (hN : ∀ (k : Fin K), List.count k (List.map Prod.fst l) / 2 < N) : timeWord l (vacCfg K N) (vacCfg K N) = wickSum l

★★ The same, with the threshold in CV-23d's form count k / 2 < N.

Consequences

theorem CSD.CV.wickSum_eq_zero_of_odd {K : ℕ} (l : List (Fin K × ℝ)) : Odd l.length → wickSum l = 0

The pairing sum of an odd word vanishes.

theorem CSD.CV.timeWord_vac_eq_zero_of_odd {K N : ℕ} [NeZero N] (l : List (Fin K × ℝ)) (hN : ∀ (k : Fin K), List.count k (List.map Prod.fst l) < 2 * N) (hl : Odd l.length) : timeWord l (vacCfg K N) (vacCfg K N) = 0

Below threshold, an odd word has no vacuum expectation.

theorem CSD.CV.wickSum_pair {K : ℕ} (x y : Fin K × ℝ) : wickSum [x, y] = contraction x y

Two insertions: the pairing sum is the one contraction.

theorem CSD.CV.wickSum_four {K : ℕ} (a b c d : Fin K × ℝ) : wickSum [a, b, c, d] = contraction a b * contraction c d + contraction a c * contraction b d + contraction a d * contraction b c

Four insertions: the three pairings.

theorem CSD.CV.contraction_natMul {K : ℕ} (τ : ℝ) (n m : ℕ) (k l : Fin K) : contraction (k, ↑n * τ) (l, ↑m * τ) = if k = l then twoPointKernel τ n m else 0

At stroboscopic times the contraction is CV-23b's kernel.

theorem CSD.CV.freeFieldU_pow_eq {K N : ℕ} (τ : ℝ) (n : ℕ) : freeFieldU K N τ ^ n = freeFieldU K N (↑n * τ)

The stroboscopic power of the free step is the free step at the multiplied time.

theorem CSD.CV.timeFourPoint_eq_wickSum {K N : ℕ} [NeZero N] (hN2 : 2 < N) (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) (k₁ k₂ k₃ k₄ : Fin K) : timeFourPoint τ n₁ n₂ n₃ n₄ k₁ k₂ k₃ k₄ = wickSum [(k₁, ↑n₁ * τ), (k₂, ↑n₂ * τ), (k₃, ↑n₃ * τ), (k₄, ↑n₄ * τ)]

★ CV-23b's time-separated four-point function is the pairing sum at stroboscopic times.

theorem CSD.CV.freeFieldU_zero {K N : ℕ} : freeFieldU K N 0 = 1

The free step at time 0 is the identity.

theorem CSD.CV.timeWord_map_zero {K N : ℕ} (l : List (Fin K)) : timeWord (List.map (fun (k : Fin K) => (k, 0)) l) = wordOp l

At time 0 the word is CV-23d's equal-time word.

theorem CSD.CV.wickSum_map_zero {K N : ℕ} [NeZero N] (l : List (Fin K)) (hN : ∀ (k : Fin K), List.count k l / 2 < N) : wickSum (List.map (fun (k : Fin K) => (k, 0)) l) = ∏ k : Fin K, wickMoment (List.count k l)

★ At equal time the pairing sum is CV-23d's Gaussian moment product: each mode contributes (count − 1)‼ / 2^{count/2}, the number of its pairings times the kernel ½ per pair.

The second-order vacuum diagrams of every monomial vertex

theorem CSD.CV.heisenberg_one_op {K N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) : heisenberg U 1 = 1

Heisenberg conjugation fixes the identity.

theorem CSD.CV.heisenberg_list_prod {K N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (l : List (Matrix (FieldConfig K N) (FieldConfig K N) ℂ)) : heisenberg U l.prod = (List.map (heisenberg U) l).prod

Heisenberg conjugation distributes over a product of operators.

theorem CSD.CV.heisenberg_wordOp {K N : ℕ} (τ : ℝ) (w : List (Fin K)) : heisenberg (freeFieldU K N τ) (wordOp w) = timeWord (List.map (fun (k : Fin K) => (k, τ)) w)

The free Heisenberg picture of an equal-time word is the word at that time.

theorem CSD.CV.dysonTerm_two_vac_wordOp {K N : ℕ} [NeZero N] (lam : ℝ) (w : List (Fin K)) (hw : ∀ (k : Fin K), List.count k w < N) (t : ℝ) : (-Complex.I • fieldHamiltonian K N).dysonTerm (-Complex.I • lam • wordOp w) 2 t (vacCfg K N) (vacCfg K N) = Complex.exp (↑t * (-Complex.I * ↑(fieldEnergy (vacCfg K N)))) * ((-Complex.I * ↑lam) ^ 2 * ∫ (s₂ : ℝ) in 0..t, ∫ (s₁ : ℝ) in 0..s₂, wickSum (List.map (fun (k : Fin K) => (k, 0)) w ++ List.map (fun (k : Fin K) => (k, s₁ - s₂)) w))

★★ The second-order vacuum diagrams of every monomial vertex. For V = Q_{k₁} ⋯ Q_{kₘ} with fewer than N insertions of every mode, the two-vertex vacuum amplitude of CV-27 is the ordered double integral of the pairing sum of the word with its copy at the time difference s₁ − s₂ — every pairing of the 2m legs of the two vertices, each a product of m propagator lines.

The matching-indexed form

theorem CSD.CV.wickSum_eq_pairingSum {K : ℕ} (l : List (Fin K × ℝ)) : wickSum l = Fin.pairingSum fun (i i' : Fin l.length) => contraction l[i] l[i']

★★ The pairing sum is the sum over perfect matchings. wickSum l is Fin.pairingSum of the contraction on the positions of l: the sum over fixed-point-free involutions σ of Fin l.length of the product over the pairs i < σ i of contraction lᵢ l_{σ i}.

theorem CSD.CV.timeWord_vac_eq_pairingSum {K N : ℕ} [NeZero N] (l : List (Fin K × ℝ)) (hN : ∀ (k : Fin K), List.count k (List.map Prod.fst l) / 2 < N) : timeWord l (vacCfg K N) (vacCfg K N) = Fin.pairingSum fun (i i' : Fin l.length) => contraction l[i] l[i']

★★ Wick's theorem at the cutoff, matching-indexed. Below threshold, the vacuum expectation of Q_{k₁}(t₁) ⋯ Q_{kₘ}(tₘ) is the sum over the perfect matchings σ of its m insertions of the product over the pairs i < σ i of the propagator lines contraction (kᵢ, tᵢ) (k_{σ i}, t_{σ i}).