CV-6: dynamical mode locality — support is invariant under free evolution

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

CV/ModeLocality.lean proved the kinematic locality axiom: operators supported on disjoint mode sets commute (commute_of_disjointSupport). This module makes it dynamical: Heisenberg evolution by the free field's stroboscopic step preserves mode support, so the commutation of disjoint regions persists at every period.

• heisenberg U A — Heisenberg conjugation U† A U, with the algebra lemmas heisenberg_one / heisenberg_mul.
• heisenberg_phaseDiagU_supportedOn — the mechanism, for ANY mode-additive diagonal phase f c = ∑ₖ g k (c k): conjugation multiplies the entry A c d by the phase e^{-i (f d − f c)}, and when c, d agree off S the phase difference collapses to the S-modes (sum_sub_sum_of_agree, star_phase_mul_phase) — so both SupportedOn fields survive.
• heisenberg_freeFieldU_supportedOn / heisenberg_freeFieldU_pow_supportedOn — the free field is mode-additive (fieldEnergy c = ∑ₖ oscEnergy (c k)), so one period — and hence every period — preserves support.
• ★★ commute_heisenberg_freeFieldU_pow — dynamical locality: observables of disjoint mode sets, evolved for any number of free-field periods, still commute. The Haag–Kastler kinematic axiom is stable under the free dynamics.

Honest scope: the free (mode-diagonal) drive only. Interacting drives are handled downstream: CV-8 bounds where support goes (CV/SupportSpreading.lean, the coupling-graph light cone, with a K = N = 2 witness), and CV-9 prices how much locality costs in norm (CV/InteractionPrice.lean, linear in the coupling).

References

CV/ModeLocality.lean (SupportedOn, commute_of_disjointSupport); CV/FreeFieldFloquet.lean (phaseDiagU, freeFieldU, CV-5); CV/FieldModes.lean (fieldEnergy); specs/external-library-map.md §H; specs/BACKLOG.md; specs/future-work.md.

Heisenberg conjugation

noncomputable def CSD.CV.heisenberg {K N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

Heisenberg conjugation by a unitary: A ↦ U† A U, the observable after one period of the dynamics generated by U.

Equations

• CSD.CV.heisenberg U A = star ↑U * A * ↑U

@[simp]

theorem CSD.CV.heisenberg_one {K N : ℕ} (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : heisenberg 1 A = A

theorem CSD.CV.heisenberg_mul {K N : ℕ} (U V : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : heisenberg (U * V) A = heisenberg V (heisenberg U A)

Conjugation by a product is iterated conjugation.

theorem CSD.CV.heisenberg_phaseDiagU_apply {K N : ℕ} (f : FieldConfig K N → ℝ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (c d : FieldConfig K N) : heisenberg (phaseDiagU f) A c d = star (Complex.exp (-(Complex.I * ↑(f c)))) * A c d * Complex.exp (-(Complex.I * ↑(f d)))

Conjugation by a diagonal-phase unitary multiplies each entry by the phase difference: (U† A U) c d = e^{+i f(c)} · A c d · e^{-i f(d)}.

Mode-additive phases and the phase-difference collapse

theorem CSD.CV.sum_sub_sum_of_agree {K N : ℕ} {S : Finset (Fin K)} (g : Fin K → Fin N → ℝ) {x y : FieldConfig K N} (h : ∀ k ∉ S, x k = y k) : ∑ k : Fin K, g k (y k) - ∑ k : Fin K, g k (x k) = ∑ k ∈ S, (g k (y k) - g k (x k))

Off-S agreement collapses a mode-additive difference to the S-modes: the spectator terms cancel.

theorem CSD.CV.star_phase_mul_phase {K N : ℕ} {S : Finset (Fin K)} (g : Fin K → Fin N → ℝ) {x y : FieldConfig K N} (h : ∀ k ∉ S, x k = y k) : star (Complex.exp (-(Complex.I * ↑(∑ k : Fin K, g k (x k))))) * Complex.exp (-(Complex.I * ↑(∑ k : Fin K, g k (y k)))) = Complex.exp (-(Complex.I * ↑(∑ k ∈ S, (g k (y k) - g k (x k)))))

The conjugating phase pair of a mode-additive diagonal unitary depends only on the S-modes when the configurations agree off S: e^{+i f(x)} · e^{-i f(y)} = e^{-i ∑_{k∈S} (g k (y k) − g k (x k))}.

theorem CSD.CV.heisenberg_phaseDiagU_supportedOn {K N : ℕ} {S : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (g : Fin K → Fin N → ℝ) (hA : SupportedOn S A) : SupportedOn S (heisenberg (phaseDiagU fun (c : FieldConfig K N) => ∑ k : Fin K, g k (c k)) A)

Mode-additive diagonal phases preserve mode support. Conjugation multiplies A c d by e^{-i (f d − f c)}; when the configurations agree off S the phase difference lives on the S-modes alone, so both SupportedOn fields survive.

The free field: support is invariant at every period

theorem CSD.CV.heisenberg_freeFieldU_supportedOn {K N : ℕ} {S : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ : ℝ) (hA : SupportedOn S A) : SupportedOn S (heisenberg (freeFieldU K N τ) A)

One free-field period preserves mode support — the field energy is mode-additive (fieldEnergy c = ∑ₖ oscEnergy (c k)).

theorem CSD.CV.heisenberg_freeFieldU_pow_supportedOn {K N : ℕ} {S : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ : ℝ) (n : ℕ) (hA : SupportedOn S A) : SupportedOn S (heisenberg (freeFieldU K N τ ^ n) A)

Every free-field period preserves mode support: the n-period Heisenberg observable is still supported on S.

theorem CSD.CV.commute_heisenberg_freeFieldU {K N : ℕ} {S T : Finset (Fin K)} (hST : Disjoint S T) {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ : ℝ) (hA : SupportedOn S A) (hB : SupportedOn T B) : heisenberg (freeFieldU K N τ) A * heisenberg (freeFieldU K N τ) B = heisenberg (freeFieldU K N τ) B * heisenberg (freeFieldU K N τ) A

Disjointly supported observables commute after one free-field period.

theorem CSD.CV.commute_heisenberg_freeFieldU_pow {K N : ℕ} {S T : Finset (Fin K)} (hST : Disjoint S T) {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ : ℝ) (n : ℕ) (hA : SupportedOn S A) (hB : SupportedOn T B) : heisenberg (freeFieldU K N τ ^ n) A * heisenberg (freeFieldU K N τ ^ n) B = heisenberg (freeFieldU K N τ ^ n) B * heisenberg (freeFieldU K N τ ^ n) A

★★ Dynamical locality: observables of disjoint mode sets, evolved in the Heisenberg picture for ANY number of free-field periods, still commute. The kinematic Haag–Kastler axiom (commute_of_disjointSupport) is stable under the free dynamics — locality is a feature of the evolution, not just of the instant.