CV-23d: Wick's theorem for an arbitrary equal-time word

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

CV/Wick.lean resolved the equal-time 2n-point function by pattern: single-mode moments (modeOpQ_pow_two_mul_vac, (2n−1)‼·(½)ⁿ for n < N), two-block factorisation (modeOpQ_pow_mul_pow_vac), and the remark that longer grouped words iterate the clustering and interleaved words commute into grouped form. This module states the resulting theorem once, for an arbitrary word of quadratures — any length, any modes, any interleaving — so that the equal-time Wick expansion is a single formula rather than a pattern table.

• wordOp l — the operator of a word l : List (Fin K) of modes, the product of the mode quadratures in the written order;
• wickMoment m — the Gaussian moment (m − 1)‼ / 2^{m/2} for even m, and 0 for odd m: the number of perfect matchings of m letters, each pairing carrying the vacuum two-point value ½;
• wordOp_eq_modeOp_pow_mul — any word is one mode's block times the word with that mode removed (the interleaving commutes out, commute_modeOp); wordOp_supportedOn — a word is supported on its modes;
• ★ wordOp_vac_eq_prod_pow — clustering: the vacuum expectation of any word is the product, over modes, of the single-mode moments of the mode's multiplicity in the word (diag_entry_mul_of_disjointSupport, block by block);
• ★★ wordOp_vac_eq_prod_wickMoment — Wick's theorem at equal time, for every word: below the truncation threshold, ⟨vac∣ Q_{k₁} ⋯ Q_{k_m} ∣vac⟩ = ∏_k wickMoment (count k); in particular the expectation vanishes whenever some mode occurs an odd number of times (wordOp_vac_eq_zero_of_odd_count), and for a word of 2n letters all of one mode it is (2n−1)‼ · (½)ⁿ.

The pairing reading. A perfect matching of the word's m letters that pairs only equal modes contributes ∏ ½ over its m/2 pairs, and there are ∏_k (count k − 1)‼ such matchings (a matching of a multiset factors over the mode classes, and a 2j-letter class has (2j−1)‼ matchings). So ∏_k wickMoment (count k) is the sum over pairings of the product of two-point functions, in the form that does not need a type of matchings. The matching-indexed sum itself is a combinatorial restatement and is not separately stated here.

Honest scope

⚠️ Equal time. Every quadrature sits at the same time; the pairing value is the vacuum fluctuation ½ and carries no phase. The time-separated formula, whose pairings carry the stroboscopic kernels K(nᵢ, nⱼ), is the four-point theorem timeFourPoint_wick and is not generalised here (the value then depends on which letters pair, so multiplicities do not determine it).

⚠️ Below the truncation threshold, count k / 2 < N for every mode k: exactly the single-mode ladder's threshold (Q_pow_two_mul_vac), because the clustering reduces the word to single-mode moments. Above it the truncated ladder is no longer Gaussian, as CV/Wick.lean documents at N = 2 and N = 3.

⚠️ The free (mode-diagonal) drive only, as for the whole Wick chain; no continuum limit (ApproxCCR.no_exact_finite_ccr).

References: CV/Wick.lean (the moment ladder and the two-block clustering); CV/Propagator.lean (diag_entry_mul_of_disjointSupport); CV/ModeLocality.lean (commute_modeOp, modeOp_supportedOn); CV/LocalAlgebra.lean (SupportedOn.mul, .mono, .one); specs/BACKLOG.md #36(b); specs/future-work.md.

The word operator and the Gaussian moment

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

The operator of a word of modes: the product of the mode quadratures, in the written order.

Equations

• CSD.CV.wordOp l = (List.map (fun (k : Fin K) => CSD.CV.modeOp k (CSD.CV.Q N)) l).prod

@[simp]

theorem CSD.CV.wordOp_nil {K N : ℕ} : wordOp [] = 1

theorem CSD.CV.wordOp_cons {K N : ℕ} (k : Fin K) (l : List (Fin K)) : wordOp (k :: l) = modeOp k (Q N) * wordOp l

noncomputable def CSD.CV.wickMoment (m : ℕ) : ℂ

The Gaussian vacuum moment of m quadratures of one mode: (m − 1)‼ / 2^{m/2} for even m, the number of perfect matchings of m letters times ½ per pair, and 0 for odd m.

Equations

• CSD.CV.wickMoment m = if Even m then ↑(m - 1).doubleFactorial / 2 ^ (m / 2) else 0

theorem CSD.CV.wickMoment_even (n : ℕ) : wickMoment (2 * n) = ↑(2 * n - 1).doubleFactorial / 2 ^ n

theorem CSD.CV.wickMoment_odd (n : ℕ) : wickMoment (2 * n + 1) = 0

theorem CSD.CV.Q_pow_vac_eq_wickMoment {N : ℕ} [NeZero N] (m : ℕ) (hm : m / 2 < N) : (Q N ^ m) 0 0 = wickMoment m

The single-mode ladder, indexed by the multiplicity: below threshold the vacuum moment of Q^m is wickMoment m.

A word is its mode blocks

theorem CSD.CV.wordOp_eq_modeOp_pow_mul {K N : ℕ} (k : Fin K) (l : List (Fin K)) : wordOp l = modeOp k (Q N ^ List.count k l) * wordOp (List.filter (fun (x : Fin K) => decide (x ≠ k)) l)

Any word is one mode's block, at that mode's multiplicity, times the word with the mode removed: the interleaved occurrences commute out past the other modes.

theorem CSD.CV.wordOp_supportedOn {K N : ℕ} (l : List (Fin K)) : SupportedOn l.toFinset (wordOp l)

A word is supported on the set of its modes.

theorem CSD.CV.modeOp_pow_vac_entry {K N : ℕ} [NeZero N] (k : Fin K) (m : ℕ) : modeOp k (Q N ^ m) (vacCfg K N) (vacCfg K N) = (Q N ^ m) 0 0

The vacuum diagonal of a single-mode block is the single-mode moment.

Clustering, and Wick's theorem for every word

theorem CSD.CV.wordOp_vac_eq_prod_pow {K N : ℕ} [NeZero N] (l : List (Fin K)) : wordOp l (vacCfg K N) (vacCfg K N) = ∏ k : Fin K, (Q N ^ List.count k l) 0 0

★ Clustering. The vacuum expectation of any word is the product over modes of the single-mode moments at the mode's multiplicity.

theorem CSD.CV.wordOp_vac_eq_prod_wickMoment {K N : ℕ} [NeZero N] (l : List (Fin K)) (hN : ∀ (k : Fin K), List.count k l / 2 < N) : wordOp l (vacCfg K N) (vacCfg K N) = ∏ k : Fin K, wickMoment (List.count k l)

★★ Wick's theorem at equal time, for every word. Below the truncation threshold, the vacuum expectation of any product of mode quadratures is the product over modes of the Gaussian moment of the mode's multiplicity: ∏_k wickMoment (count k), which is the sum over perfect matchings pairing equal modes of ½ per pair.

theorem CSD.CV.wordOp_vac_eq_prod_wickMoment_of_length {K N : ℕ} [NeZero N] (l : List (Fin K)) (hN : l.length / 2 < N) : wordOp l (vacCfg K N) (vacCfg K N) = ∏ k : Fin K, wickMoment (List.count k l)

The length form of the threshold: length / 2 < N suffices for every mode.

theorem CSD.CV.wordOp_vac_eq_zero_of_odd_count {K N : ℕ} [NeZero N] (l : List (Fin K)) {k : Fin K} (hk : Odd (List.count k l)) : wordOp l (vacCfg K N) (vacCfg K N) = 0

A word in which some mode occurs an odd number of times has vanishing vacuum expectation.

theorem CSD.CV.wordOp_replicate_vac {K N : ℕ} [NeZero N] (k : Fin K) (n : ℕ) (hn : n < N) : wordOp (List.replicate (2 * n) k) (vacCfg K N) (vacCfg K N) = ↑(2 * n - 1).doubleFactorial / 2 ^ n

The all-one-mode word of 2n letters: (2n−1)‼ · (½)ⁿ, the moment ladder recovered.