CV-23b: the time-separated four-point function — Wick's theorem with the phases on

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

Glossary: https://glossary.constraintsurfacedynamics.com/wick-theorem/ Plain-language, CSD-role and formal statements of Wick's theorem at the cutoff, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

CV-22/CV-23a proved Wick's four-point theorem at equal times (eqFourPoint_wick); CV-13 computed the two-point function with one factor evolved (freeTwoPoint_eq). This module joins them: each quadrature at its own Heisenberg period, and the four-point function equal to the pairing sum over stroboscopic kernels.

• twoPointKernel τ n m — the stroboscopic kernel K(n,m) = ½·e^{-inτ}·e^{+imτ}, kept in two-factor form so ℕ-subtraction never appears. twoPointKernel_self (= ½, the equal-time vacuum fluctuation) and twoPointKernel_zero_right (the CV-13 propagator value at right period 0).

• timeTwoPoint τ n m k l — ⟨vac∣Q_k(n)·Q_l(m)∣vac⟩, both factors evolved. ★ timeTwoPoint_eq — the two-time propagator: = δ_{kl}·K(n,m), diagonal in the mode index; timeTwoPoint_zero_right recovers freeTwoPoint at the definition level.

• timeFourPoint τ n₁ n₂ n₃ n₄ k₁ k₂ k₃ k₄ — ⟨vac∣Q_{k₁}(n₁)·Q_{k₂}(n₂)·Q_{k₃}(n₃)·Q_{k₄}(n₄)∣vac⟩, resolved by coincidence pattern exactly as the equal-time table: a singleton mode kills it (timeFourPoint_single₁–₄), the two-pair patterns give the kernel product of the paired times (_pair/_alt/_outer — the arrangement now carries content the equal-time table could not see: which times meet in a kernel is decided by the pairing), and the all-equal pattern is the three-pairing sum (★ timeFourPoint_same, 2 < N).

• ★★ timeFourPoint_wick — Wick's four-point theorem at distinct times: above the truncation threshold 2 < N,

  ⟨Q_{k₁}(n₁)Q_{k₂}(n₂)Q_{k₃}(n₃)Q_{k₄}(n₄)⟩ = δ_{k₁k₂}δ_{k₃k₄}·K₁₂K₃₄ + δ_{k₁k₃}δ_{k₂k₄}·K₁₃K₂₄ + δ_{k₁k₄}δ_{k₂k₃}·K₁₄K₂₃,

  one formula over every mode pattern, with K_{ij} = twoPointKernel τ n_i n_j. All periods 0 (or the formula at equal periods, via twoPointKernel_self) recover CV-23a: timeFourPoint_zero.

• The CV-23c gate — the six-point pass (equal time): ★ modeOpQ_six_vac — the sixth moment ⟨vac∣Q_k⁶∣vac⟩ = 15/8 = 5!!·(½)³ for 3 < N, via the Q³ column at the vacuum (modeOpQ_cube_apply_vac — the plan's ‖Q³e₀‖² anchor, computed in walk-collapse form); modeOpQ_four_two_vac — the mixed pattern ⟨Q_k⁴·Q_l²⟩ = 3/8 by clustering into eqFourPoint_same. At N = 3 the level-3 walk dies and the all-equal value is 9/8, not 15/8 — the threshold honesty one rung up, guarded by 3 < N. The idiom scaled by exactly one rung (one configuration, one entry-ladder level, one reachability lemma, fin_cases-free): the gate passes.

• The 2n-point closure (CV-23c): ★★ Q_pow_two_mul_vac and its field-level form modeOpQ_pow_two_mul_vac — the moment ladder: below the truncation threshold the vacuum moments of the quadrature are exactly Gaussian, ⟨vac∣Q_k^{2n}∣vac⟩ = (2n−1)‼·(½)ⁿ for n < N. (2n−1)‼ counts Wick's pairings of 2n insertions, each pairing carrying (½)ⁿ; the threshold is n < N shaped exactly as scoped — a 2n-step return walk reaches at most level n, so the cutoff is invisible iff n < N. Proved by the commutator recursion ⟨Q^{2n+2}⟩ = (2n+1)/2·⟨Q^{2n}⟩ (Q_pow_vac_recursion) against the truncated CCR (truncated_ccr), the rank-one defect killed by the walk band (Q_pow_apply_vac_of_lt: at most one of the two sandwich entries can reach the top level). Odd moments vanish by walk parity (modeOpQ_pow_two_mul_add_one_vac). ★ modeOpQ_pow_mul_pow_vac: grouped two-block patterns factorise into single-mode moments; longer grouped words iterate the same clustering, and arbitrary interleavings reduce to grouped form mode-by-mode via commute_modeOp.

Why Wick survives truncation exactly (the load-bearing identity): the all-equal pattern is one level-2 walk 0→1→2→1→0 with amplitude ½·e^{-i(t₁+t₂−t₃−t₄)}, and the two cross-pairings K₁₃K₂₄ and K₁₄K₂₃ are each ¼·e^{-i(t₁+t₂−t₃−t₄)} — their sum IS the walk term. At N = 2 the walk dies and only K₁₂K₃₄ survives: the 2 < N hypothesis is load-bearing exactly where eqFourPoint_same says.

⚠️ Honest scope: the free (mode-diagonal) drive only, matching freeTwoPoint's scope; interacting corrections are priced by the CV-9/CV-12 ladder (twoPoint_interacting_dist_le) and not restated. No continuum limit (ApproxCCR.no_exact_finite_ccr stands). The 2n-point closure is pattern-resolved: single-mode moments (Q_pow_two_mul_vac) plus two-block factorisation (modeOpQ_pow_mul_pow_vac), from which any grouped multi-mode word follows by iterating the clustering, and any interleaved word by first commuting distinct modes (commute_modeOp) into grouped form. The one-shot combinatorial pairing-sum formula over an arbitrary 2n-letter word (a sum over perfect matchings) is not separately stated — (2n−1)‼ carries that content on the mode diagonal, and the four-point case has it explicitly (eqFourPoint_wick, timeFourPoint_wick). Equal-time only: the time-separated story above stops at four points. The relativistic reading is the CV-13 substitution (relFieldHamiltonian, spacing ω(m, p)), recorded not restated.

References

specs/eft-stage7-plan.md (row CV-23b — the construction notes this module executes: the two-factor kernel, the cross-pairing exponent identity, the brick list); specs/BACKLOG.md (Q21); specs/future-work.md (row CV-23); CV/Propagator.lean (eqFourPoint and its coincidence table, eqFourPoint_wick, freeTwoPoint_eq, diag_entry_mul_of_disjointSupport, the Q entry ladder); CV/ThermalPropagator.lean (heisenberg_freeFieldU_pow_apply, sum_collapse_of_support); CV/Oscillator.lean (truncated_ccr — the engine of the moment recursion; annihilation_apply/creation_apply, topProj); Mathlib/Data/Nat/Factorial/DoubleFactorial.lean (Nat.doubleFactorial); CV/ModeLocality.lean (commute_of_disjointSupport, modeOp_supportedOn); CV/DynamicalLocality.lean (heisenberg_freeFieldU_pow_supportedOn); CONVENTIONS.md §8.3b (the pattern lemmas feed the one packaged capstone).

The stroboscopic kernel

noncomputable def CSD.CV.twoPointKernel (τ : ℝ) (n m : ℕ) : ℂ

The stroboscopic two-point kernel K(n,m) = ½·e^{-inτ}·e^{+imτ}, the value of the two-time propagator on the mode diagonal. Kept in two-factor form (never e^{-i(n-m)τ}) so ℕ-subtraction does not appear.

Equations

• CSD.CV.twoPointKernel τ n m = 2⁻¹ * Complex.exp (-(Complex.I * ↑(↑n * τ))) * Complex.exp (Complex.I * ↑(↑m * τ))

theorem CSD.CV.twoPointKernel_self (τ : ℝ) (n : ℕ) : twoPointKernel τ n n = 2⁻¹

Equal periods: the kernel is the equal-time vacuum fluctuation ½.

theorem CSD.CV.twoPointKernel_zero_right (τ : ℝ) (n : ℕ) : twoPointKernel τ n 0 = 2⁻¹ * Complex.exp (-(Complex.I * ↑(↑n * τ)))

Right period 0: the kernel is CV-13's propagator value ½·e^{-inτ} (freeTwoPoint_eq's diagonal entry).

theorem CSD.CV.inv_sqrt_two_mul_self : (↑√2)⁻¹ * (↑√2)⁻¹ = 2⁻¹

(√2)⁻¹·(√2)⁻¹ = 2⁻¹ in ℂ — the squared hop amplitude.

The energy step to the two-quantum level

theorem CSD.CV.fieldEnergy_exc2Cfg_sub {K N : ℕ} [NeZero N] (hN2 : 2 < N) (hN : 1 < N) (l : Fin K) : fieldEnergy (exc2Cfg hN2 l) - fieldEnergy (excCfg hN l) = 1

The second quantum also costs one unit of free energy: E(exc2 l) − E(exc l) = 1.

The evolved quadrature's hop entries

The free evolution decorates each modeOp k (Q N) entry with the phase e^{inτ(E_c − E_d)} (heisenberg_freeFieldU_pow_apply); on the four hops the walk uses, the energy difference is ±1 and the phase is e^{∓inτ}.

theorem CSD.CV.evolvedQ_apply_vac {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n : ℕ) (k : Fin K) {e : FieldConfig K N} (he : e ≠ excCfg hN k) : heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) e (vacCfg K N) = 0

The evolved quadrature reaches the vacuum only from the one-quantum configuration: the phase decoration does not move the support (column form).

theorem CSD.CV.evolvedQ_vac_apply {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n : ℕ) (k : Fin K) {e : FieldConfig K N} (he : e ≠ excCfg hN k) : heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) (vacCfg K N) e = 0

Row form: from the vacuum, the evolved quadrature reaches only the one-quantum configuration.

theorem CSD.CV.evolvedQ_vac_exc {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n : ℕ) (k : Fin K) : heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) (vacCfg K N) (excCfg hN k) = Complex.exp (-(Complex.I * ↑(↑n * τ))) * (↑√2)⁻¹

The up-hop from the vacuum: Q_k(n)(vac, exc) = e^{-inτ}·(√2)⁻¹.

theorem CSD.CV.evolvedQ_exc_vac {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n : ℕ) (k : Fin K) : heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) (excCfg hN k) (vacCfg K N) = Complex.exp (Complex.I * ↑(↑n * τ)) * (↑√2)⁻¹

The down-hop to the vacuum: Q_k(n)(exc, vac) = e^{+inτ}·(√2)⁻¹.

theorem CSD.CV.evolvedQ_exc_exc2 {K N : ℕ} [NeZero N] (hN2 : 2 < N) (hN : 1 < N) (τ : ℝ) (n : ℕ) (k : Fin K) : heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) (excCfg hN k) (exc2Cfg hN2 k) = Complex.exp (-(Complex.I * ↑(↑n * τ)))

The up-hop into the two-quantum level: Q_k(n)(exc, exc2) = e^{-inτ} (the ladder amplitude √2/√2 = 1).

theorem CSD.CV.evolvedQ_exc2_exc {K N : ℕ} [NeZero N] (hN2 : 2 < N) (hN : 1 < N) (τ : ℝ) (n : ℕ) (k : Fin K) : heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) (exc2Cfg hN2 k) (excCfg hN k) = Complex.exp (Complex.I * ↑(↑n * τ))

The down-hop from the two-quantum level: Q_k(n)(exc2, exc) = e^{+inτ}.

The evolved pair: entries of Q_k(n)·Q_k(m) at the vacuum

theorem CSD.CV.evolvedPair_vac_vac {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n m : ℕ) (k : Fin K) : (heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) * heisenberg (freeFieldU K N τ ^ m) (modeOp k (Q N))) (vacCfg K N) (vacCfg K N) = twoPointKernel τ n m

The evolved pair's vacuum diagonal IS the kernel: (Q_k(n)·Q_k(m))(vac, vac) = K(n,m) — one up-hop, one down-hop.

theorem CSD.CV.evolvedPair_vac_vac_offdiag {K N : ℕ} [NeZero N] (τ : ℝ) (n m : ℕ) {k l : Fin K} (hkl : k ≠ l) : (heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) * heisenberg (freeFieldU K N τ ^ m) (modeOp l (Q N))) (vacCfg K N) (vacCfg K N) = 0

Distinct modes have no vacuum two-point correlation, whatever the periods: clustering plus the quadrature's missing vacuum diagonal.

theorem CSD.CV.evolvedPair_apply_vac_of_ne {K N : ℕ} [NeZero N] (hN2 : 2 < N) (hN : 1 < N) (τ : ℝ) (n m : ℕ) (k : Fin K) {e : FieldConfig K N} (h0 : e ≠ vacCfg K N) (h2 : e ≠ exc2Cfg hN2 k) : (heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) * heisenberg (freeFieldU K N τ ^ m) (modeOp k (Q N))) e (vacCfg K N) = 0

The evolved pair's column at the vacuum is supported on the vacuum and the two-quantum configuration — the only three-hop walks from level 1 end at levels 0 and 2.

theorem CSD.CV.evolvedPair_vac_exc2 {K N : ℕ} [NeZero N] (hN2 : 2 < N) (hN : 1 < N) (τ : ℝ) (n m : ℕ) (k : Fin K) : (heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) * heisenberg (freeFieldU K N τ ^ m) (modeOp k (Q N))) (vacCfg K N) (exc2Cfg hN2 k) = (↑√2)⁻¹ * (Complex.exp (-(Complex.I * ↑(↑n * τ))) * Complex.exp (-(Complex.I * ↑(↑m * τ))))

The evolved pair's entry into the two-quantum configuration: (Q_k(n)·Q_k(m))(vac, exc2) = (√2)⁻¹·e^{-inτ}·e^{-imτ} — two up-hops.

theorem CSD.CV.evolvedPair_exc2_vac {K N : ℕ} [NeZero N] (hN2 : 2 < N) (hN : 1 < N) (τ : ℝ) (n m : ℕ) (k : Fin K) : (heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) * heisenberg (freeFieldU K N τ ^ m) (modeOp k (Q N))) (exc2Cfg hN2 k) (vacCfg K N) = (↑√2)⁻¹ * (Complex.exp (Complex.I * ↑(↑n * τ)) * Complex.exp (Complex.I * ↑(↑m * τ)))

The evolved pair's return from the two-quantum configuration: (Q_k(n)·Q_k(m))(exc2, vac) = (√2)⁻¹·e^{+inτ}·e^{+imτ} — two down-hops.

The two-time propagator

noncomputable def CSD.CV.timeTwoPoint {K N : ℕ} [NeZero N] (τ : ℝ) (n m : ℕ) (k l : Fin K) : ℂ

The time-separated two-point function ⟨vac∣Q_k(n)·Q_l(m)∣vac⟩: both quadratures in the Heisenberg picture, each at its own period.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.CV.timeTwoPoint_eq {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n m : ℕ) (k l : Fin K) : timeTwoPoint τ n m k l = if k = l then twoPointKernel τ n m else 0

★ The two-time propagator: ⟨vac∣Q_k(n)·Q_l(m)∣vac⟩ = δ_{kl}·K(n,m) — diagonal in the mode index, the kernel at the two periods on the diagonal.

theorem CSD.CV.timeTwoPoint_zero_right {K N : ℕ} [NeZero N] (τ : ℝ) (n : ℕ) (k l : Fin K) : timeTwoPoint τ n 0 k l = freeTwoPoint τ n k l

Right period 0 recovers CV-13's freeTwoPoint at the definition level.

The time-separated four-point function

noncomputable def CSD.CV.timeFourPoint {K N : ℕ} [NeZero N] (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) (k₁ k₂ k₃ k₄ : Fin K) : ℂ

The time-separated four-point function ⟨vac∣Q_{k₁}(n₁)·Q_{k₂}(n₂)·Q_{k₃}(n₃)·Q_{k₄}(n₄)∣vac⟩ — every quadrature at its own Heisenberg period under the free stroboscopic dynamics.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.CV.timeFourPoint_zero {K N : ℕ} [NeZero N] (τ : ℝ) (k₁ k₂ k₃ k₄ : Fin K) : timeFourPoint τ 0 0 0 0 k₁ k₂ k₃ k₄ = eqFourPoint k₁ k₂ k₃ k₄

All periods 0 recover the equal-time four-point function (CV-22/CV-23a).

theorem CSD.CV.commute_evolvedQ {K N : ℕ} [NeZero N] (τ : ℝ) (n m : ℕ) {k l : Fin K} (hkl : k ≠ l) : heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) * heisenberg (freeFieldU K N τ ^ m) (modeOp l (Q N)) = heisenberg (freeFieldU K N τ ^ m) (modeOp l (Q N)) * heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N))

Evolved quadratures at distinct modes commute, whatever their periods — the Haag–Kastler locality of commute_modeOp, transported through the free evolution (heisenberg_freeFieldU_pow_supportedOn).

theorem CSD.CV.timeFourPoint_single₁ {K N : ℕ} [NeZero N] (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) {k₁ k₂ k₃ k₄ : Fin K} (h1 : k₁ ≠ k₂) (h2 : k₁ ≠ k₃) (h3 : k₁ ≠ k₄) : timeFourPoint τ n₁ n₂ n₃ n₄ k₁ k₂ k₃ k₄ = 0

A mode appearing once (first position) kills the time-separated expectation: the evolved quadrature has no vacuum diagonal, and clustering isolates it.

theorem CSD.CV.timeFourPoint_single₂ {K N : ℕ} [NeZero N] (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) {k₁ k₂ k₃ k₄ : Fin K} (h1 : k₂ ≠ k₁) (h2 : k₂ ≠ k₃) (h3 : k₂ ≠ k₄) : timeFourPoint τ n₁ n₂ n₃ n₄ k₁ k₂ k₃ k₄ = 0

A mode appearing once (second position) kills the expectation.

theorem CSD.CV.timeFourPoint_single₃ {K N : ℕ} [NeZero N] (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) {k₁ k₂ k₃ k₄ : Fin K} (h1 : k₃ ≠ k₁) (h2 : k₃ ≠ k₂) (h3 : k₃ ≠ k₄) : timeFourPoint τ n₁ n₂ n₃ n₄ k₁ k₂ k₃ k₄ = 0

A mode appearing once (third position) kills the expectation.

theorem CSD.CV.timeFourPoint_single₄ {K N : ℕ} [NeZero N] (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) {k₁ k₂ k₃ k₄ : Fin K} (h1 : k₄ ≠ k₁) (h2 : k₄ ≠ k₂) (h3 : k₄ ≠ k₃) : timeFourPoint τ n₁ n₂ n₃ n₄ k₁ k₂ k₃ k₄ = 0

A mode appearing once (fourth position) kills the expectation.

theorem CSD.CV.timeFourPoint_pair {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) {k l : Fin K} (hkl : k ≠ l) : timeFourPoint τ n₁ n₂ n₃ n₄ k k l l = twoPointKernel τ n₁ n₂ * twoPointKernel τ n₃ n₄

★ Two pairs, grouped: ⟨Q_k(n₁)Q_k(n₂)Q_l(n₃)Q_l(n₄)⟩ = K(n₁,n₂)·K(n₃,n₄) for k ≠ l — the one surviving Wick pairing, via clustering (diag_entry_mul_of_disjointSupport).

theorem CSD.CV.timeFourPoint_alt {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) {k l : Fin K} (hkl : k ≠ l) : timeFourPoint τ n₁ n₂ n₃ n₄ k l k l = twoPointKernel τ n₁ n₃ * twoPointKernel τ n₂ n₄

Two pairs, alternating: ⟨Q_k(n₁)Q_l(n₂)Q_k(n₃)Q_l(n₄)⟩ = K(n₁,n₃)·K(n₂,n₄) — commuting the disjoint modes pairs the times (n₁,n₃) and (n₂,n₄): the arrangement decides which times meet in a kernel.

theorem CSD.CV.timeFourPoint_outer {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n₁ n₂ n₃ n₄ : ℕ) {k l : Fin K} (hkl : k ≠ l) : timeFourPoint τ n₁ n₂ n₃ n₄ k l l k = twoPointKernel τ n₁ n₄ * twoPointKernel τ n₂ n₃

Two pairs, nested: ⟨Q_k(n₁)Q_l(n₂)Q_l(n₃)Q_k(n₄)⟩ = K(n₁,n₄)·K(n₂,n₃).

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

★ All four equal: the three-pairing sum ⟨Q_k(n₁)Q_k(n₂)Q_k(n₃)Q_k(n₄)⟩ = K₁₂K₃₄ + K₁₃K₂₄ + K₁₄K₂₃ for 2 < N. The walk through the vacuum gives K₁₂K₃₄; the level-2 walk 0→1→2→1→0 gives ½e^{-i(t₁+t₂−t₃−t₄)}, which is exactly K₁₃K₂₄ + K₁₄K₂₃ — the cross-pairings share one exponent, and that identity is why Wick survives truncation. At N = 2 the level-2 walk is cut off, exactly as in eqFourPoint_same.

theorem CSD.CV.timeFourPoint_wick {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₄ = (((if k₁ = k₂ then twoPointKernel τ n₁ n₂ else 0) * if k₃ = k₄ then twoPointKernel τ n₃ n₄ else 0) + (if k₁ = k₃ then twoPointKernel τ n₁ n₃ else 0) * if k₂ = k₄ then twoPointKernel τ n₂ n₄ else 0) + (if k₁ = k₄ then twoPointKernel τ n₁ n₄ else 0) * if k₂ = k₃ then twoPointKernel τ n₂ n₃ else 0

★★ Wick's four-point theorem at distinct times (CV-23b): above the truncation threshold 2 < N, the time-separated four-point function IS the pairing sum over stroboscopic kernels,

⟨Q_{k₁}(n₁)Q_{k₂}(n₂)Q_{k₃}(n₃)Q_{k₄}(n₄)⟩ = δ_{k₁k₂}δ_{k₃k₄}·K₁₂K₃₄ + δ_{k₁k₃}δ_{k₂k₄}·K₁₃K₂₄ + δ_{k₁k₄}δ_{k₂k₃}·K₁₄K₂₃,

one formula over every mode pattern, with K_{ij} = twoPointKernel τ n_i n_j the two-time propagator value (timeTwoPoint_eq). Equal periods collapse every kernel to ½ (twoPointKernel_self) and recover eqFourPoint_wick; all periods 0 recover it at the definition level (timeFourPoint_zero). The 2 < N hypothesis is load-bearing exactly where the equal-time table says: only the all-equal pattern's level-2 walk needs it.

The CV-23c gate: the six-point pass

The go/no-go probe for the 2n-point Wick theorem, agreed in advance (eft-stage7-plan.md): the six-point all-equal pattern and one mixed pattern must land with the walk-collapse idiom, fin_cases-free, thresholds explicit. The idiom scales by exactly one rung: one new configuration (exc3Cfg), one new level of the Q entry ladder (Q_two_three/Q_three_two), one new reachability lemma (modeOp_Q_apply_exc2), and the Q³ column at the vacuum. The general 2n-point theorem is NOT claimed here — the gate un-gates it.

theorem CSD.CV.Q_two_three {N : ℕ} [NeZero N] (hN3 : 3 < N) : Q N ⟨2, ⋯⟩ ⟨3, hN3⟩ = (↑√2)⁻¹ * ↑√3

Q connects the second to the third level with amplitude √3/√2.

theorem CSD.CV.Q_three_two {N : ℕ} [NeZero N] (hN3 : 3 < N) : Q N ⟨3, hN3⟩ ⟨2, ⋯⟩ = (↑√2)⁻¹ * ↑√3

Q connects the third level back to the second with the same amplitude.

theorem CSD.CV.Q_apply_two_eq_zero {N : ℕ} [NeZero N] (hN2 : 2 < N) {m : Fin N} (h1 : ↑m ≠ 1) (h3 : ↑m ≠ 3) : Q N m ⟨2, hN2⟩ = 0

Q reaches the second level only from the first and the third.

def CSD.CV.exc3Cfg {K N : ℕ} [NeZero N] (hN3 : 3 < N) (l : Fin K) : FieldConfig K N

The three-quantum configuration at mode l.

Equations

• CSD.CV.exc3Cfg hN3 l = Function.update (CSD.CV.vacCfg K N) l ⟨3, hN3⟩

@[simp]

theorem CSD.CV.exc3Cfg_self {K N : ℕ} [NeZero N] (hN3 : 3 < N) (l : Fin K) : exc3Cfg hN3 l l = ⟨3, hN3⟩

theorem CSD.CV.exc3Cfg_of_ne {K N : ℕ} [NeZero N] (hN3 : 3 < N) {l j : Fin K} (h : j ≠ l) : exc3Cfg hN3 l j = 0

theorem CSD.CV.excCfg_ne_exc3Cfg {K N : ℕ} [NeZero N] (hN3 : 3 < N) (hN : 1 < N) (k : Fin K) : excCfg hN k ≠ exc3Cfg hN3 k

theorem CSD.CV.modeOp_Q_apply_exc2 {K N : ℕ} [NeZero N] (hN3 : 3 < N) (hN2 : 2 < N) (hN : 1 < N) (k : Fin K) {e : FieldConfig K N} (h1 : e ≠ excCfg hN k) (h3 : e ≠ exc3Cfg hN3 k) : modeOp k (Q N) e (exc2Cfg hN2 k) = 0

From the two-quantum configuration, the mode quadrature reaches only the one- and three-quantum configurations.

theorem CSD.CV.modeOpQ_transpose {K N : ℕ} [NeZero N] (k : Fin K) : (modeOp k (Q N)).transpose = modeOp k (Q N)

The mode quadrature is symmetric as a matrix transpose identity.

theorem CSD.CV.modeOpQ_cube_symm {K N : ℕ} [NeZero N] (k : Fin K) (c d : FieldConfig K N) : (modeOp k (Q N) * modeOp k (Q N) * modeOp k (Q N)) c d = (modeOp k (Q N) * modeOp k (Q N) * modeOp k (Q N)) d c

The cube of the mode quadrature is symmetric — powers of a symmetric matrix stay symmetric, entrywise form.

theorem CSD.CV.modeOpQ_cube_apply_vac {K N : ℕ} [NeZero N] (hN3 : 3 < N) (hN2 : 2 < N) (hN : 1 < N) (k : Fin K) (e : FieldConfig K N) : (modeOp k (Q N) * modeOp k (Q N) * modeOp k (Q N)) e (vacCfg K N) = if e = excCfg hN k then 3 / 2 * (↑√2)⁻¹ else if e = exc3Cfg hN3 k then ↑√3 * 2⁻¹ else 0

The column of Q_k³ at the vacuum — the plan's Q³e₀ = (3/(2√2))·e₁ + (√3/2)·e₃ anchor, in walk-collapse form: mass (3/2)·(√2)⁻¹ on the one-quantum configuration, √3/2 on the three-quantum configuration, nothing else.

theorem CSD.CV.modeOpQ_six_vac {K N : ℕ} [NeZero N] (hN3 : 3 < N) (k : Fin K) : (modeOp k (Q N) ^ 6) (vacCfg K N) (vacCfg K N) = 15 / 8

★ The six-point pass, all-equal pattern: the equal-time sixth moment ⟨vac∣Q_k⁶∣vac⟩ = 15/8 = 5!!·(½)³ for 3 < N — Wick's fifteen pairings, all surviving at (½)³ each. Via ‖Q³e₀‖² = 9/8 + 3/4: the walk through the one-quantum configuration squared plus the walk through the three-quantum configuration squared. At N = 3 the level-3 walk dies and the value is 9/8 — the truncation honesty one rung above eqFourPoint_same's.

theorem CSD.CV.modeOpQ_four_two_vac {K N : ℕ} [NeZero N] (hN2 : 2 < N) {k l : Fin K} (hkl : k ≠ l) : (modeOp k (Q N) ^ 4 * modeOp l (Q N) ^ 2) (vacCfg K N) (vacCfg K N) = 3 / 8

The six-point pass, mixed pattern: ⟨vac∣Q_k⁴·Q_l²∣vac⟩ = 3/8 = (3/4)·(1/2) for k ≠ l — clustering splits the modes, and the factors are the four-point all-equal value and the vacuum fluctuation. Needs only 2 < N (the thresholds of its factors).

The 2n-point closure: the moment ladder

The gate passed; this section lands the closure it un-gated. The heart is the single-mode statement: below the truncation threshold the vacuum moments of the quadrature are exactly Gaussian, ⟨0∣Q^{2n}∣0⟩ = (2n−1)‼·(½)ⁿ for n < N, where (2n−1)‼ counts Wick's pairings. The proof is the commutator recursion ⟨Q^{2n+2}⟩ = (2n+1)/2·⟨Q^{2n}⟩ against the truncated CCR [a,a†] = 1 − N·topProj: the CCR's rank-one defect is sandwiched as ⟨0∣Q^j·topProj·Q^i∣0⟩ with i + j = 2n, and the walk band kills it — a j-step walk from the vacuum reaches at most level j, and i + j = 2n < 2(N−1) means at most one of the two factors can reach the top level. That inequality IS the n < N threshold: truncation is invisible exactly while no return walk needs the ceiling. Odd moments vanish by walk parity. modeOp is multiplicative, so the single-mode ladder transports verbatim to the field, and clustering resolves the grouped multi-mode patterns.

theorem CSD.CV.commutator_pow_expand {R : Type u_1} [Ring R] (A B : R) (m : ℕ) : A * B ^ m - B ^ m * A = ∑ j ∈ Finset.range m, B ^ j * (A * B - B * A) * B ^ (m - 1 - j)

The commutator telescopes through a power: [A, Bᵐ] = Σ_{j<m} Bʲ·[A,B]·B^{m−1−j} — a generic ring identity.

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

Q is strictly tridiagonal: entries vanish off the two hop diagonals.

theorem CSD.CV.Q_transpose {N : ℕ} [NeZero N] : (Q N).transpose = Q N

The quadrature is symmetric as a transpose identity.

theorem CSD.CV.Q_pow_apply_vac_of_lt {N : ℕ} [NeZero N] (j : ℕ) {m : Fin N} : j < ↑m → (Q N ^ j) m 0 = 0

The walk band (column form): a j-step walk from the vacuum reaches at most level j, so the power's column at the vacuum vanishes above the band.

theorem CSD.CV.Q_pow_vac_apply_of_lt {N : ℕ} [NeZero N] (j : ℕ) {m : Fin N} (h : j < ↑m) : (Q N ^ j) 0 m = 0

The walk band, row form (by symmetry of the quadrature).

theorem CSD.CV.Q_pow_apply_vac_parity {N : ℕ} [NeZero N] (j : ℕ) {m : Fin N} : ↑m % 2 ≠ j % 2 → (Q N ^ j) m 0 = 0

Walk parity: a j-step walk from the vacuum lands only on levels of j's parity.

theorem CSD.CV.Q_pow_two_mul_add_one_vac {N : ℕ} [NeZero N] (n : ℕ) : (Q N ^ (2 * n + 1)) 0 0 = 0

Odd moments vanish at the single-mode level: ⟨0∣Q^{2n+1}∣0⟩ = 0, no threshold needed.

theorem CSD.CV.annihilation_Q_commutator {N : ℕ} [NeZero N] : annihilation N * Q N - Q N * annihilation N = (↑√2)⁻¹ • (1 - ↑N • topProj N)

The ladder–quadrature commutator at the cutoff: [a, Q] = (√2)⁻¹·(1 − N·topProj) — the truncated CCR, one hop down the ladder.

theorem CSD.CV.mul_topProj_mul_apply {N : ℕ} [NeZero N] (hlt : N - 1 < N) (X Y : Matrix (Fin N) (Fin N) ℂ) : (X * topProj N * Y) 0 0 = X 0 ⟨N - 1, hlt⟩ * Y ⟨N - 1, hlt⟩ 0

The defect sandwich reads one row and one column at the top level: (X·topProj·Y)(0,0) = X(0, N−1)·Y(N−1, 0).

theorem CSD.CV.Q_pow_vac_recursion {N : ℕ} [NeZero N] (n : ℕ) (hn : n + 1 < N) : (Q N ^ (2 * n + 2)) 0 0 = ↑(2 * n + 1) / 2 * (Q N ^ (2 * n)) 0 0

★ The moment recursion below threshold: ⟨0∣Q^{2n+2}∣0⟩ = (2n+1)/2 · ⟨0∣Q^{2n}∣0⟩ for n + 1 < N. The (2n+1) counts the partners the leftmost insertion can pair with; the ½ is the pairing's kernel; the CCR defect dies because i + j = 2n < 2(N−1) lets at most one sandwich factor reach the top level.

theorem CSD.CV.Q_pow_two_mul_vac {N : ℕ} [NeZero N] (n : ℕ) : n < N → (Q N ^ (2 * n)) 0 0 = ↑(2 * n - 1).doubleFactorial / 2 ^ n

★★ The 2n-point theorem at a single mode (the CV-23c closure): below the truncation threshold the vacuum moments of the quadrature are exactly Gaussian,

⟨0∣Q^{2n}∣0⟩ = (2n−1)‼ · (½)ⁿ for n < N,

(2n−1)‼ counting Wick's pairings of the 2n insertions, each pairing carrying (½)ⁿ. The threshold is n < N shaped: a 2n-step return walk from the vacuum reaches at most level n, so the cutoff is invisible exactly while n < N — at n = N the value departs (the gate documents ⟨Q⁶⟩ = 9/8 ≠ 15/8 at N = 3).

Transport to the field

theorem CSD.CV.modeOp_one {K N : ℕ} (k : Fin K) : modeOp k 1 = 1

modeOp sends the identity to the identity.

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

modeOp is multiplicative on a fixed mode: single-mode matrices compose before or after embedding, indifferently.

theorem CSD.CV.modeOp_pow {K N : ℕ} (k : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) (m : ℕ) : modeOp k a ^ m = modeOp k (a ^ m)

modeOp respects powers.

theorem CSD.CV.modeOpQ_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

A power of the mode quadrature reads its vacuum diagonal at the single-mode level.

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

★★ The 2n-point theorem on the field (CV-23c): the equal-time vacuum moments of any mode quadrature are exactly Gaussian below threshold, ⟨vac∣Q_k^{2n}∣vac⟩ = (2n−1)‼·(½)ⁿ for n < N.

theorem CSD.CV.modeOpQ_pow_two_mul_add_one_vac {K N : ℕ} [NeZero N] (n : ℕ) (k : Fin K) : (modeOp k (Q N) ^ (2 * n + 1)) (vacCfg K N) (vacCfg K N) = 0

Odd moments vanish on the field: ⟨vac∣Q_k^{2n+1}∣vac⟩ = 0.

theorem CSD.CV.modeOpQ_pow_mul_pow_vac {K N : ℕ} [NeZero N] {k l : Fin K} (hkl : k ≠ l) (m₁ m₂ : ℕ) : (modeOp k (Q N) ^ m₁ * modeOp l (Q N) ^ m₂) (vacCfg K N) (vacCfg K N) = (Q N ^ m₁) 0 0 * (Q N ^ m₂) 0 0

★ Grouped patterns factorise: ⟨vac∣Q_k^{m₁}·Q_l^{m₂}∣vac⟩ splits into single-mode moments for k ≠ l. Longer grouped words iterate this clustering block by block, and arbitrary interleavings reduce to grouped form via commute_modeOp — together with the moment ladder, this is the equal-time 2n-point function pattern-resolved.