CV-24: the thermal tier at the cutoff — Gibbs field state, thermal propagator, exact KMS

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

Glossary: https://glossary.constraintsurfacedynamics.com/kms-condition/ Plain-language, CSD-role and formal statements of the KMS condition, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The first join of the two complete verticals: the Thermo track's Gibbs state (TH3, Thermo/FreeEnergy.lean) instantiated on the CV track's free-field Hamiltonian. Every temperature statement below is about that state — the object the TH3 variational principle governs — not a separately posited Boltzmann matrix.

• thermalFieldState β — gibbsState (fieldHamiltonian K N) _ β, THE TH3 Gibbs state on the field. Because fieldHamiltonian is diagonal, the state has a closed form: ★ thermalFieldState_eq — the diagonal Boltzmann matrix with weights exp(-β·E(c)) / fieldPartition, obtained through cfc_eq_conj_diagonal at the trivial unitary; fieldPartition_eq_partitionFn reconciles the configuration-basis partition function with TH3's eigenvalue form via the trace normalisation.

• fieldPartition_eq_pow — the partition function factorises over modes, Z_field = z_osc^K, and ★ thermalExpect_modeOp is the thermal mode marginal: the thermal expectation of a single-mode observable is its single-mode Gibbs expectation — the thermal analogue of modeMarginal_tprod_unit.

• thermalEvolve z — Heisenberg evolution at complex time, entrywise e^{iz(E_c − E_d)}·A_{cd}; total and well-defined at every z : ℂ because the Hamiltonian is diagonal and the dimension finite — no analytic-continuation apparatus. thermalEvolve_real_eq_heisenberg ties the real-time slice to the CV chain's own stroboscopic evolution heisenberg (freeFieldU τ ^ n).

• ★★ thermal_kms — exact KMS at the cutoff, the corpus's first KMS statement: ⟨A(t)·B⟩_β = ⟨B·A(t+iβ)⟩_β for all matrices A, B, all t, β. At finite dimension with a diagonal Hamiltonian the identity is an entrywise exponential shuffle — the weight transport w_c = w_d·e^{-β(E_c−E_d)} — exactly as the Stage-7 feasibility check predicted.

• thermalTwoPoint β τ n k l — the thermal two-point function of the quadratures, ⟨Q_k(n)·Q_l⟩_β under the free stroboscopic dynamics. thermalTwoPoint_offdiag: modes do not mix thermally (= 0 for k ≠ l — the thermal companion of the vacuum propagator's δ_{kl}). ★ thermalTwoPoint_diag — the closed form: a single-mode Boltzmann average of one up-step and one down-step,

  ⟨Q_k(n)Q_k⟩_β = (1/z_osc)·∑_a e^{-β(a+½)}·( (a+1)/2·e^{-inτ}·[a+1<N] + a/2·e^{+inτ} ),

  with the truncation edge explicit: the top level a = N−1 has no up-step, so the [a+1<N] guard is the same truncation honesty the vacuum four-point's 2 < N carries.

• ★ thermalTwoPoint_tendsto_vacuum — the vacuum limit: as β → ∞ the thermal propagator converges to freeTwoPoint — the zero-point energies cancel between numerator and partition function, the reduced weights are geometric, and the ground level dominates. Finite sums only; no dominated convergence.

Honest scope

The free (mode-diagonal) drive only, matching freeTwoPoint's scope; interacting corrections are priced by the CV-9/CV-12 ladder and not restated thermally. No continuum limit (ApproxCCR.no_exact_finite_ccr stands) and no thermodynamic limit in K: every statement is at the finite cutoff, where it is exact. The relativistic reading is the same substitution as CV-13 (relFieldHamiltonian, spacing ω(m,p)), recorded not restated. The β → ∞ vacuum limit is landed (thermalTwoPoint_tendsto_vacuum), so CV-24 carries no recorded residue.

References

specs/eft-stage7-plan.md (row CV-24, the feasibility record this executes); specs/BACKLOG.md (Q21); Thermo/FreeEnergy.lean (gibbsState, gibbsWeight, partitionFn, gibbsState_trace); Mathlib/QuantumInfo/Subadditivity.lean (cfc_eq_conj_diagonal); CV/Propagator.lean (freeTwoPoint, the walk-collapse idiom, diag_entry_mul_of_disjointSupport); CV/DynamicalLocality.lean (heisenberg, heisenberg_phaseDiagU_apply); CV/FreeFieldFloquet.lean (phaseDiagU, freeFieldU); CV/InteractionPrice.lean (fieldHamiltonian_isHermitian).

The thermal field state and its closed form

noncomputable def CSD.CV.thermalFieldState (K N : ℕ) (β : ℝ) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The thermal field state: the TH3 Gibbs state ρ_β = e^{-βH}/Z instantiated on the free-field Hamiltonian — the Thermo↔CV join.

Equations

• CSD.CV.thermalFieldState K N β = CSD.Thermo.gibbsState (CSD.CV.fieldHamiltonian K N) ⋯ β

noncomputable def CSD.CV.fieldPartition (β : ℝ) (K N : ℕ) : ℝ

The configuration-basis partition function ∑_c e^{-β·E(c)}.

Equations

• CSD.CV.fieldPartition β K N = ∑ c : CSD.CV.FieldConfig K N, Real.exp (-β * CSD.CV.fieldEnergy c)

noncomputable def CSD.CV.oscPartition (β : ℝ) (N : ℕ) : ℝ

The single-mode partition function z = ∑_m e^{-β·(m+½)}.

Equations

• CSD.CV.oscPartition β N = ∑ m : Fin N, Real.exp (-β * CSD.CV.oscEnergy ↑m)

noncomputable def CSD.CV.thermalWeight {K N : ℕ} (β : ℝ) (c : FieldConfig K N) : ℝ

The Boltzmann weight of a configuration.

Equations

• CSD.CV.thermalWeight β c = Real.exp (-β * CSD.CV.fieldEnergy c) / CSD.CV.fieldPartition β K N

theorem CSD.CV.oscPartition_pos {N : ℕ} [NeZero N] (β : ℝ) : 0 < oscPartition β N

theorem CSD.CV.thermalFieldState_eq_gibbs_diagonal {K N : ℕ} (β : ℝ) : thermalFieldState K N β = Matrix.diagonal fun (c : FieldConfig K N) => ↑(Thermo.gibbsWeight (fieldHamiltonian K N) ⋯ β (fieldEnergy c))

The Gibbs state of the diagonal Hamiltonian is diagonal, with the Gibbs weights of the configuration energies on the diagonal — cfc_eq_conj_diagonal at U = 1.

theorem CSD.CV.fieldPartition_eq_partitionFn {K N : ℕ} [NeZero N] (β : ℝ) : fieldPartition β K N = Thermo.partitionFn (fieldHamiltonian K N) ⋯ β

The configuration-basis partition function agrees with TH3's eigenvalue form — extracted from the trace normalisation Tr ρ_β = 1.

theorem CSD.CV.thermalFieldState_eq {K N : ℕ} [NeZero N] (β : ℝ) : thermalFieldState K N β = Matrix.diagonal fun (c : FieldConfig K N) => ↑(thermalWeight β c)

★ The thermal field state, in closed form: the diagonal Boltzmann matrix.

Thermal expectations

noncomputable def CSD.CV.thermalExpect {K N : ℕ} (β : ℝ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : ℂ

The thermal expectation ⟨A⟩_β = Tr(ρ_β A).

Equations

• CSD.CV.thermalExpect β A = (CSD.CV.thermalFieldState K N β * A).trace

theorem CSD.CV.thermalExpect_eq {K N : ℕ} [NeZero N] (β : ℝ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : thermalExpect β A = ∑ c : FieldConfig K N, ↑(thermalWeight β c) * A c c

The thermal expectation is the Boltzmann-weighted diagonal sum.

Complex-time evolution and exact KMS

noncomputable def CSD.CV.thermalEvolve {K N : ℕ} (z : ℂ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

Heisenberg evolution at complex time under the free-field Hamiltonian, entrywise e^{iz(E_c − E_d)}·A_{cd}. Total at every z : ℂ: the Hamiltonian is diagonal and the dimension finite, so no analytic continuation is involved.

Equations

• CSD.CV.thermalEvolve z A = Matrix.of fun (c d : CSD.CV.FieldConfig K N) => Complex.exp (Complex.I * z * (↑(CSD.CV.fieldEnergy c) - ↑(CSD.CV.fieldEnergy d))) * A c d

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

The Heisenberg entry formula for the n-period free evolution, in phase-difference form.

theorem CSD.CV.thermalEvolve_real_eq_heisenberg {K N : ℕ} (τ : ℝ) (n : ℕ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : thermalEvolve (↑(↑n * τ)) A = heisenberg (freeFieldU K N τ ^ n) A

The real-time slice of the complex-time evolution IS the CV chain's stroboscopic Heisenberg evolution.

theorem CSD.CV.thermalWeight_transport {K N : ℕ} (β : ℝ) (c d : FieldConfig K N) : thermalWeight β c = thermalWeight β d * Real.exp (-β * (fieldEnergy c - fieldEnergy d))

The Boltzmann-weight transport identity: w_c = w_d · e^{-β(E_c − E_d)}.

theorem CSD.CV.thermal_kms {K N : ℕ} [NeZero N] (β t : ℝ) (A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : thermalExpect β (thermalEvolve (↑t) A * B) = thermalExpect β (B * thermalEvolve (↑t + Complex.I * ↑β) A)

★★ Exact KMS at the cutoff. For every pair of observables and every t, β,

⟨A(t)·B⟩_β = ⟨B·A(t+iβ)⟩_β.

The corpus's first KMS statement. At finite dimension with the diagonal free-field Hamiltonian the identity is an entrywise exponential shuffle: the iβ shift converts the Boltzmann weight at c into the weight at d (thermalWeight_transport), and the double sum relabels. Exact — no approximation, no continuation, no cutoff error.

The mode marginal

theorem CSD.CV.boltzmann_prod {K N : ℕ} (β : ℝ) (c : FieldConfig K N) : ↑(Real.exp (-β * fieldEnergy c)) = ∏ j : Fin K, ↑(Real.exp (-β * oscEnergy ↑(c j)))

The Boltzmann factor of a configuration is the product of its per-mode factors.

theorem CSD.CV.fieldPartition_eq_pow (β : ℝ) (K N : ℕ) : fieldPartition β K N = oscPartition β N ^ K

The partition function factorises over modes: Z_field = z_osc^K.

theorem CSD.CV.sum_boltzmann_mul_comp {K N : ℕ} [NeZero N] (β : ℝ) (k : Fin K) (g : Fin N → ℂ) : ∑ c : FieldConfig K N, ↑(Real.exp (-β * fieldEnergy c)) * g (c k) = ↑(oscPartition β N) ^ (K - 1) * ∑ m : Fin N, ↑(Real.exp (-β * oscEnergy ↑m)) * g m

The distinguished-coordinate factorisation: summing a Boltzmann-weighted function of one mode over all configurations splits off that mode's Gibbs sum, the spectator modes contributing one partition factor each.

theorem CSD.CV.thermalExpect_comp_mode {K N : ℕ} [NeZero N] (β : ℝ) (k : Fin K) (g : Fin N → ℂ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (hA : ∀ (c : FieldConfig K N), A c c = g (c k)) : thermalExpect β A = (∑ m : Fin N, ↑(Real.exp (-β * oscEnergy ↑m)) * g m) / ↑(oscPartition β N)

The common tail: the thermal expectation of any observable whose diagonal reads a single mode is the single-mode Gibbs average of that reading — the factorisation engine both the mode marginal and the two-point closed form consume.

theorem CSD.CV.thermalExpect_modeOp {K N : ℕ} [NeZero N] (β : ℝ) (k : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) : thermalExpect β (modeOp k a) = (∑ m : Fin N, ↑(Real.exp (-β * oscEnergy ↑m)) * a m m) / ↑(oscPartition β N)

★ The thermal mode marginal: the thermal expectation of a single-mode observable is its single-mode Gibbs expectation — the thermal analogue of modeMarginal_tprod_unit.

The thermal two-point function

theorem CSD.CV.Q_apply_self {N : ℕ} [NeZero N] (m : Fin N) : Q N m m = 0

The quadrature has zero diagonal: Q is strictly tridiagonal.

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

The thermal two-point function ⟨Q_k(n)·Q_l⟩_β: the mode-k quadrature evolved n free periods, against the mode-l quadrature, in the thermal state.

Equations

• CSD.CV.thermalTwoPoint β τ n k l = CSD.CV.thermalExpect β (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))

theorem CSD.CV.thermalTwoPoint_offdiag {K N : ℕ} [NeZero N] (β τ : ℝ) (n : ℕ) {k l : Fin K} (hkl : k ≠ l) : thermalTwoPoint β τ n k l = 0

Modes do not mix thermally: the thermal two-point function vanishes off the mode diagonal — the thermal companion of the vacuum propagator's δ_{kl}.

theorem CSD.CV.sum_collapse_of_support {K N : ℕ} (c : FieldConfig K N) (k : Fin K) (F : FieldConfig K N → ℂ) (h0 : ∀ (d : FieldConfig K N), (¬∀ (j : Fin K), j ≠ k → c j = d j) → F d = 0) : ∑ d : FieldConfig K N, F d = ∑ m : Fin N, F (Function.update c k m)

Collapse of a configuration sum against mode-k locality: a summand vanishing off "agrees with c away from k" reduces to a sum over the mode-k value.

theorem CSD.CV.fieldEnergy_update {K N : ℕ} (c : FieldConfig K N) (k : Fin K) (m : Fin N) : fieldEnergy (Function.update c k m) = fieldEnergy c - oscEnergy ↑(c k) + oscEnergy ↑m

The field energy of a one-mode update.

theorem CSD.CV.Q_mul_Q_apply {N : ℕ} (a m : Fin N) : Q N a m * Q N m a = if ↑a + 1 = ↑m then ↑↑m / 2 else if ↑m + 1 = ↑a then ↑↑a / 2 else 0

The two-sided quadrature entry product: Q_{am}·Q_{ma} is m/2 on the up-step m = a+1, a/2 on the down-step m+1 = a, and 0 elsewhere.

theorem CSD.CV.qWalk_eval {N : ℕ} [NeZero N] (θ : ℝ) (a : Fin N) : ∑ m : Fin N, Complex.exp (Complex.I * ↑θ * (↑(oscEnergy ↑a) - ↑(oscEnergy ↑m))) * (Q N a m * Q N m a) = (if ↑a + 1 < N then ↑(↑a + 1) / 2 * Complex.exp (-(Complex.I * ↑θ)) else 0) + ↑↑a / 2 * Complex.exp (Complex.I * ↑θ)

The single-mode thermal walk: the phase-weighted quadrature return sum evaluates to one up-step and one down-step. The up-step exists only below the cutoff ceiling — the [a+1 < N] guard is the truncation honesty of eqFourPoint_same's 2 < N, here at every level.

theorem CSD.CV.evolved_mul_modeOpQ_diag {K N : ℕ} [NeZero N] (τ : ℝ) (n : ℕ) (k : Fin K) (c : FieldConfig K N) : (heisenberg (freeFieldU K N τ ^ n) (modeOp k (Q N)) * modeOp k (Q N)) c c = ∑ m : Fin N, Complex.exp (Complex.I * ↑(↑n * τ) * (↑(oscEnergy ↑(c k)) - ↑(oscEnergy ↑m))) * (Q N (c k) m * Q N m (c k))

The diagonal entry of the evolved-against-static quadrature product is a single-mode walk at the configuration's mode-k level — the two-point analogue of the vacuum computation, at every configuration.

theorem CSD.CV.thermalTwoPoint_diag {K N : ℕ} [NeZero N] (β τ : ℝ) (n : ℕ) (k : Fin K) : thermalTwoPoint β τ n k k = (∑ a : Fin N, ↑(Real.exp (-β * oscEnergy ↑a)) * ((if ↑a + 1 < N then ↑(↑a + 1) / 2 * Complex.exp (-(Complex.I * ↑(↑n * τ))) else 0) + ↑↑a / 2 * Complex.exp (Complex.I * ↑(↑n * τ)))) / ↑(oscPartition β N)

★ The thermal two-point function, in closed form. On the mode diagonal the thermal propagator is a single-mode Boltzmann average of one up-step and one down-step:

⟨Q_k(n)Q_k⟩_β = (1/z)·∑_a e^{-β(a+½)}·( (a+1)/2·e^{-inτ}·[a+1<N] + a/2·e^{+inτ} ).

The truncation edge is explicit — the top level has no up-step — and at β → ∞ the a = 0 term dominates, recovering the vacuum propagator ½·e^{-inτ} (freeTwoPoint_eq); the interacting correction rides the CV-9/CV-12 price unchanged.

theorem CSD.CV.thermalTwoPoint_tendsto_vacuum {K N : ℕ} [NeZero N] (hN : 1 < N) (τ : ℝ) (n : ℕ) (k : Fin K) : Filter.Tendsto (fun (β : ℝ) => thermalTwoPoint β τ n k k) Filter.atTop (nhds (freeTwoPoint τ n k k))

★ The vacuum limit. As β → ∞ the thermal propagator converges to the vacuum propagator: the ground level dominates the Boltzmann average, and the closed form's a = 0 term is exactly freeTwoPoint's ½·e^{-inτ}. The zero-point energies cancel between numerator and partition function, so the limit is a statement about the reduced geometric weights e^{-βa} — finite sums, no dominated convergence.