CV-13: the finite free propagator — the chain computes a correlation function

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

Every EFT statement so far has been structural (locality, cones) or a bound (prices, power counting). This module produces the chain's first computed observable: the free field's two-point function, in closed form, oscillating at the excitation energy.

• vacCfg / excCfg — the vacuum configuration and the one-quantum configuration at mode l.
• fieldEnergy_excCfg_sub — the excitation costs exactly one energy quantum: E(exc l) − E(vac) = 1 (the free spacing; under relFieldHamiltonian the same computation gives ω(m, p_l), recorded below).
• phaseDiagU_pow / freeFieldU_pow — a diagonal-phase drive's n-th power is the drive at n-fold phase (so the Heisenberg entry formula applies at every period).
• freeTwoPoint τ n k l — the two-point function ⟨vac| Q_k(n) Q_l |vac⟩, with Q_k(n) the CV-6 Heisenberg evolution of the mode-k quadrature under n free periods.
• ★★ freeTwoPoint_eq — the lattice propagator: freeTwoPoint τ n k l = (1/2)·e^{-i n τ}·δ_{kl}. Diagonal in the mode index (free modes do not mix), and oscillating at the excitation energy — the dispersion appearing as an observable time dependence rather than a spectrum label. freeTwoPoint_zero fixes the equal-time normalisation 1/2 (the vacuum quadrature fluctuation), and norm_freeTwoPoint shows the modulus is period-independent: the free propagator does not decay.
• ★ twoPoint_interacting_dist_le — switching on a diagonal interaction moves the two-point function by at most 2n·|τ|·|λ|·C·‖Q‖²: the Born-approximation error, priced by the CV-9/CV-12 ladder.

⚠️ Honest scope: the free (or diagonal-drive) two-point function at a finite cutoff, for the quadrature observables — not a general Wightman function, and no continuum limit (no_exact_finite_ccr stands). The relativistic reading is a substitution, not a separate theorem: replacing fieldHamiltonian by relFieldHamiltonian replaces the spacing 1 by ω(m, p_l) in the same computation (CV/Dispersion.lean, relFieldEnergy_quantum), recorded as the CV-13 residue.

References

CV/FieldModes.lean (fieldEnergy); CV/Oscillator.lean (Q, the ladder entries); CV/ModeLocality.lean (modeOp); CV/DynamicalLocality.lean (heisenberg_phaseDiagU_apply); CV/InteractionPrice.lean (CV-9, the price); specs/eft-stage4-plan.md (row CV-13); specs/future-work.md.

The vacuum and one-quantum configurations

def CSD.CV.vacCfg (K N : ℕ) [NeZero N] : FieldConfig K N

The vacuum configuration: every mode unoccupied.

Equations

• CSD.CV.vacCfg K N x✝ = 0

def CSD.CV.excCfg {K N : ℕ} [NeZero N] (hN : 1 < N) (l : Fin K) : FieldConfig K N

The one-quantum configuration at mode l.

Equations

• CSD.CV.excCfg hN l = Function.update (CSD.CV.vacCfg K N) l ⟨1, hN⟩

@[simp]

theorem CSD.CV.vacCfg_apply {K N : ℕ} [NeZero N] (k : Fin K) : vacCfg K N k = 0

@[simp]

theorem CSD.CV.excCfg_self {K N : ℕ} [NeZero N] (hN : 1 < N) (l : Fin K) : excCfg hN l l = ⟨1, hN⟩

theorem CSD.CV.excCfg_of_ne {K N : ℕ} [NeZero N] (hN : 1 < N) {l j : Fin K} (h : j ≠ l) : excCfg hN l j = 0

theorem CSD.CV.excCfg_agree {K N : ℕ} [NeZero N] (hN : 1 < N) (l : Fin K) {j : Fin K} (h : j ≠ l) : excCfg hN l j = vacCfg K N j

Off its own mode, the one-quantum configuration agrees with the vacuum.

theorem CSD.CV.eq_excCfg {K N : ℕ} [NeZero N] (hN : 1 < N) {l : Fin K} {c : FieldConfig K N} (hoff : ∀ (j : Fin K), j ≠ l → c j = vacCfg K N j) (hat : ↑(c l) = 1) : c = excCfg hN l

A configuration agreeing with the vacuum off l and carrying one quantum at l IS the one-quantum configuration.

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

★ One quantum costs one unit of free energy: E(exc l) − E(vac) = 1.

Powers of a diagonal-phase drive

theorem CSD.CV.phaseDiagU_pow {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : ι → ℝ) (n : ℕ) : phaseDiagU f ^ n = phaseDiagU fun (x : ι) => ↑n * f x

The n-th power of a diagonal-phase unitary is the drive at n-fold phase.

theorem CSD.CV.freeFieldU_pow (K N : ℕ) (τ : ℝ) (n : ℕ) : freeFieldU K N τ ^ n = phaseDiagU fun (c : FieldConfig K N) => ↑n * (τ * fieldEnergy c)

The free drive at period count n.

The quadrature entries at the vacuum

theorem CSD.CV.Q_zero_one {N : ℕ} [NeZero N] (hN : 1 < N) : Q N 0 ⟨1, hN⟩ = (↑√2)⁻¹

Q connects the vacuum to the first excited level with amplitude 1/√2.

theorem CSD.CV.Q_one_zero {N : ℕ} [NeZero N] (hN : 1 < N) : Q N ⟨1, hN⟩ 0 = (↑√2)⁻¹

Q connects the first excited level back to the vacuum with the same amplitude.

theorem CSD.CV.Q_apply_zero_eq_zero {N : ℕ} [NeZero N] {m : Fin N} (hm : ↑m ≠ 1) : Q N m 0 = 0

Q annihilates the vacuum except through the first excited level.

theorem CSD.CV.norm_exp_neg_I_mul_real (r : ℝ) : ‖Complex.exp (-(Complex.I * ↑r))‖ = 1

A pure phase has unit modulus.

The two-point function

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

The free two-point function: ⟨vac| Q_k(n) Q_l |vac⟩, with Q_k(n) the Heisenberg evolution of the mode-k quadrature under n free periods.

Equations

• CSD.CV.freeTwoPoint τ n k l = (CSD.CV.heisenberg (CSD.CV.freeFieldU K N τ ^ n) (CSD.CV.modeOp k (CSD.CV.Q N)) * CSD.CV.modeOp l (CSD.CV.Q N)) (CSD.CV.vacCfg K N) (CSD.CV.vacCfg K N)

theorem CSD.CV.modeOp_Q_apply_vac {K N : ℕ} [NeZero N] (hN : 1 < N) (l : Fin K) (e : FieldConfig K N) (he : e ≠ excCfg hN l) : modeOp l (Q N) e (vacCfg K N) = 0

The one-quantum configuration is the only intermediate state the right-hand quadrature reaches from the vacuum.

theorem CSD.CV.freeTwoPoint_eq {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n : ℕ) (k l : Fin K) : freeTwoPoint τ n k l = if k = l then 2⁻¹ * Complex.exp (-(Complex.I * ↑(↑n * τ))) else 0

★★ The lattice propagator. The free two-point function is diagonal in the mode index and oscillates at the excitation energy: ⟨vac| Q_k(n) Q_l |vac⟩ = (1/2)·e^{-i n τ}·δ_{kl}.

theorem CSD.CV.freeTwoPoint_zero {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (k : Fin K) : freeTwoPoint τ 0 k k = 2⁻¹

The equal-time normalisation: the vacuum quadrature fluctuation is 1/2 on the diagonal.

theorem CSD.CV.norm_freeTwoPoint {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n : ℕ) (k : Fin K) : ‖freeTwoPoint τ n k k‖ = 1 / 2

The free propagator does not decay: its modulus is independent of the period count (all the dynamics is in the phase).

The interacting correction, priced

noncomputable def CSD.CV.interactingTwoPoint {K N : ℕ} [NeZero N] (τ lam : ℝ) (v : FieldConfig K N → ℝ) (n : ℕ) (k l : Fin K) : ℂ

The two-point function under the interacting drive.

Equations

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

theorem CSD.CV.twoPoint_interacting_dist_le {K N : ℕ} [NeZero N] (τ lam : ℝ) (v : FieldConfig K N → ℝ) {C : ℝ} (hC : 0 ≤ C) (hv : ∀ (c : FieldConfig K N), |v c| ≤ C) (n : ℕ) (k l : Fin K) : ‖interactingTwoPoint τ lam v n k l - freeTwoPoint τ n k l‖ ≤ 2 * (↑n * (|τ| * (|lam| * C))) * ‖modeOp k (Q N)‖ * ‖modeOp l (Q N)‖

★ The Born-approximation error, priced: switching on a diagonal interaction moves the two-point function by at most 2n·|τ|·|λ|·C·‖Q_k‖·‖Q_l‖ — the CV-9 Duhamel price carried through the CV-12 unitary telescoping and the entrywise bound.

CV-21 (Stage 6): vacuum clustering — correlations are local too

The dynamic cone (CV-18/19/20) says signals cannot cross disjoint supports faster than the coupling allows. The statics companion: at the cutoff, correlations across disjoint supports do not exist at all in the vacuum — expectations factorise exactly. The proof is the same uniqueness of the intermediate configuration that powers commute_of_disjointSupport: between two visits to the same configuration, an R-supported and a Y-supported operator admit only the trivial intermediate.

theorem CSD.CV.diag_entry_mul_of_disjointSupport {K N : ℕ} [NeZero N] {R Y : Finset (Fin K)} (hRY : Disjoint R Y) {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) (hB : SupportedOn Y B) (v : FieldConfig K N) : (A * B) v v = A v v * B v v

Diagonal entries multiply across disjoint supports: for any configuration v, (A·B)(v,v) = A(v,v)·B(v,v) when A and B live on disjoint mode sets — the only intermediate configuration both tolerate is v itself.

theorem CSD.CV.vacuum_clustering {K N : ℕ} [NeZero N] {R Y : Finset (Fin K)} (hRY : Disjoint R Y) {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) (hB : SupportedOn Y B) : (A * B) (vacCfg K N) (vacCfg K N) = A (vacCfg K N) (vacCfg K N) * B (vacCfg K N) (vacCfg K N)

★★ Vacuum clustering at the cutoff (CV-21, Stage 6): vacuum expectations of disjointly supported observables factorise exactly, ⟨vac∣AB∣vac⟩ = ⟨vac∣A∣vac⟩·⟨vac∣B∣vac⟩. There are no vacuum correlations across disjoint mode sets — the statics companion to the Lieb–Robinson cone: at the cutoff, correlations, like signals, are local.

CV-22 (Stage 6): the four-point Wick table

The equal-time four-point function ⟨vac∣Q_k Q_l Q_m Q_p∣vac⟩, resolved by coincidence pattern. Every 4-tuple of modes falls into exactly one of: some mode appears once (eqFourPoint_single₁–₄: the expectation vanishes — every Wick pairing would carry a mismatched δ), two pairs in any arrangement (eqFourPoint_pair/_alt/_outer: = 1/4, the one surviving pairing (½)²), or all four equal (eqFourPoint_same: = 3/4 = 3·(½)², all three pairings surviving). These are exactly Wick's values Σ_pairings ∏ G with G(a,b) = ½δ_{ab} (freeTwoPoint at n = 0) — the table IS the four-point Wick theorem at the cutoff, stated pattern-resolved; the packaged single-formula δ-sum is a recorded packaging residue (assembly, not mathematics). Truncation honesty: the all-equal case needs 2 < N (the walk visits the two-quantum level — at N = 2 the value is 1/4, not 3/4); the two-pair cases need only 1 < N. Higher 2n-point Wick is not claimed.

theorem CSD.CV.Q_zero_zero {N : ℕ} [NeZero N] : Q N 0 0 = 0

Q vanishes on the vacuum diagonal.

theorem CSD.CV.Q_one_two {N : ℕ} [NeZero N] (hN2 : 2 < N) : Q N ⟨1, ⋯⟩ ⟨2, hN2⟩ = 1

Q connects the first to the second level with amplitude 1 (√2/√2).

theorem CSD.CV.Q_two_one {N : ℕ} [NeZero N] (hN2 : 2 < N) : Q N ⟨2, hN2⟩ ⟨1, ⋯⟩ = 1

Q connects the second level back to the first with amplitude 1.

theorem CSD.CV.Q_apply_one_eq_zero {N : ℕ} [NeZero N] (hN : 1 < N) {m : Fin N} (h0 : ↑m ≠ 0) (h2 : ↑m ≠ 2) : Q N m ⟨1, hN⟩ = 0

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

theorem CSD.CV.Q_symm {N : ℕ} [NeZero N] (i j : Fin N) : Q N i j = Q N j i

The quadrature is a symmetric matrix.

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

The mode quadrature is a symmetric matrix.

def CSD.CV.exc2Cfg {K N : ℕ} [NeZero N] (hN2 : 2 < N) (l : Fin K) : FieldConfig K N

The two-quantum configuration at mode l.

Equations

• CSD.CV.exc2Cfg hN2 l = Function.update (CSD.CV.vacCfg K N) l ⟨2, hN2⟩

@[simp]

theorem CSD.CV.exc2Cfg_self {K N : ℕ} [NeZero N] (hN2 : 2 < N) (l : Fin K) : exc2Cfg hN2 l l = ⟨2, hN2⟩

theorem CSD.CV.exc2Cfg_of_ne {K N : ℕ} [NeZero N] (hN2 : 2 < N) {l j : Fin K} (h : j ≠ l) : exc2Cfg hN2 l j = 0

theorem CSD.CV.vacCfg_ne_exc2Cfg {K N : ℕ} [NeZero N] (hN2 : 2 < N) (k : Fin K) : vacCfg K N ≠ exc2Cfg hN2 k

theorem CSD.CV.modeOp_Q_apply_exc {K N : ℕ} [NeZero N] (hN2 : 2 < N) (k : Fin K) {e : FieldConfig K N} (h0 : e ≠ vacCfg K N) (h2 : e ≠ exc2Cfg hN2 k) : modeOp k (Q N) e (excCfg ⋯ k) = 0

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

theorem CSD.CV.modeOpQ_sq_vac {K N : ℕ} [NeZero N] (hN : 1 < N) (k : Fin K) : (modeOp k (Q N) * modeOp k (Q N)) (vacCfg K N) (vacCfg K N) = 2⁻¹

The equal-time single-mode second moment: (Q_k²)(vac, vac) = 1/2.

theorem CSD.CV.modeOpQ_sq_apply_vac {K N : ℕ} [NeZero N] (hN2 : 2 < N) (k : Fin K) (e : FieldConfig K N) : (modeOp k (Q N) * modeOp k (Q N)) e (vacCfg K N) = if e = vacCfg K N then 2⁻¹ else if e = exc2Cfg hN2 k then (↑√2)⁻¹ else 0

The column of Q_k² at the vacuum: mass 1/2 on the vacuum, 1/√2 on the two-quantum configuration, nothing else.

theorem CSD.CV.modeOpQ_sq_exc2_vac {K N : ℕ} [NeZero N] (hN2 : 2 < N) (k : Fin K) : (modeOp k (Q N) * modeOp k (Q N)) (exc2Cfg hN2 k) (vacCfg K N) = (↑√2)⁻¹

The Q_k² column value at the two-quantum configuration.

noncomputable def CSD.CV.eqFourPoint {K N : ℕ} [NeZero N] (k l m p : Fin K) : ℂ

The equal-time four-point function ⟨vac∣ Q_k Q_l Q_m Q_p ∣vac⟩.

Equations

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

theorem CSD.CV.eqFourPoint_same {K N : ℕ} [NeZero N] (hN2 : 2 < N) (k : Fin K) : eqFourPoint k k k k = 3 / 4

★★ All four equal: ⟨vac∣Q_k⁴∣vac⟩ = 3/4 — Wick's three pairings of ½ each, and the first place the two-quantum level enters (2 < N required: at N = 2 the value is 1/4).

theorem CSD.CV.eqFourPoint_pair {K N : ℕ} [NeZero N] (hN : 1 < N) {k l : Fin K} (hkl : k ≠ l) : eqFourPoint k k l l = 1 / 4

★★ Two pairs, grouped: ⟨vac∣Q_k²Q_l²∣vac⟩ = 1/4 for k ≠ l — the one surviving Wick pairing, via clustering (diag_entry_mul_of_disjointSupport).

theorem CSD.CV.eqFourPoint_alt {K N : ℕ} [NeZero N] (hN : 1 < N) {k l : Fin K} (hkl : k ≠ l) : eqFourPoint k l k l = 1 / 4

Two pairs, alternating: ⟨vac∣Q_kQ_lQ_kQ_l∣vac⟩ = 1/4 — the commutation of disjoint modes reduces it to the grouped case.

theorem CSD.CV.eqFourPoint_outer {K N : ℕ} [NeZero N] (hN : 1 < N) {k l : Fin K} (hkl : k ≠ l) : eqFourPoint k l l k = 1 / 4

Two pairs, nested: ⟨vac∣Q_kQ_lQ_lQ_k∣vac⟩ = 1/4.

theorem CSD.CV.eqFourPoint_single₁ {K N : ℕ} [NeZero N] {k l m p : Fin K} (h1 : k ≠ l) (h2 : k ≠ m) (h3 : k ≠ p) : eqFourPoint k l m p = 0

A mode appearing once (first position) kills the expectation: Q has no vacuum diagonal, and clustering isolates it.

theorem CSD.CV.eqFourPoint_single₂ {K N : ℕ} [NeZero N] {k l m p : Fin K} (h1 : l ≠ k) (h2 : l ≠ m) (h3 : l ≠ p) : eqFourPoint k l m p = 0

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

theorem CSD.CV.eqFourPoint_single₃ {K N : ℕ} [NeZero N] {k l m p : Fin K} (h1 : m ≠ k) (h2 : m ≠ l) (h3 : m ≠ p) : eqFourPoint k l m p = 0

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

theorem CSD.CV.eqFourPoint_single₄ {K N : ℕ} [NeZero N] {k l m p : Fin K} (h1 : p ≠ k) (h2 : p ≠ l) (h3 : p ≠ m) : eqFourPoint k l m p = 0

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

theorem CSD.CV.eqFourPoint_wick {K N : ℕ} [NeZero N] (hN2 : 2 < N) (k l m p : Fin K) : eqFourPoint k l m p = (((if k = l then 2⁻¹ else 0) * if m = p then 2⁻¹ else 0) + (if k = m then 2⁻¹ else 0) * if l = p then 2⁻¹ else 0) + (if k = p then 2⁻¹ else 0) * if l = m then 2⁻¹ else 0

★★ Wick's four-point theorem at the cutoff, packaged (CV-23a): above the truncation threshold 2 < N the equal-time four-point function IS the pairing sum

⟨Q_k Q_l Q_m Q_p⟩ = Σ_pairings ∏ ½δ = ¼(δ_{kl}δ_{mp} + δ_{km}δ_{lp} + δ_{kp}δ_{lm}),

one formula over every mode pattern — the coincidence-pattern table (eqFourPoint_same, _pair/_alt/_outer, _single₁–₄) assembled into the textbook shape. The 2 < N hypothesis is load-bearing exactly where the table says: at N = 2 the all-equal pattern is 1/4, not the Gaussian 3/4, and the formula fails — truncation honesty, not a technical convenience.