CV-11: the non-diagonal light cone — exp-closure of the local algebra

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

CV-8's light cone covered diagonal (density) couplings. This module removes that restriction: the local algebra is topologically closed, so the exponential of a locally supported generator is locally supported, and the coupling-graph light cone extends to kicked drives with arbitrary — non-diagonal, hopping — local kicks.

• SupportedOn.zero, localSubmodule T, localAlgebra T — the local algebra packaged as a Submodule/Subalgebra (from the CV-8 closure lemmas), with isClosed_localSubmodule: a subspace of a finite-dimensional matrix space is closed.
• ★ SupportedOn.exp — exp-closure: exp of a T-supported matrix is T-supported (every partial sum of the exponential series lives in the algebra; the limit stays by closedness).
• KickData / KickData.ofGenerator — a local kick as a unitary supported on an edge; the smart constructor builds it from any skew-Hermitian edge-supported generator (expKick_unitary + exp-closure), so hopping generators like i(a†ₖaₗ − a†ₗaₖ) are now admissible.
• kickFoldStep / kickFold — the per-period support growth of a kick LIST: each kick enlarges the region by its edge exactly when it touches (heisenberg_eq_of_disjoint keeps untouched kicks trivial), and sequential kicks may chain within a period — the fold records that honestly. For a single kick, or kicks touching disjoint regions, the fold reduces to CV-8's graphNeighborhood-style growth.
• ★★ heisenberg_kickedStep_pow_supportedOn — the non-diagonal light cone: after n periods of the kicked drive (free step + the kick list), support lies inside the n-fold kickFold ball. With commute_heisenberg_kickedStep_pow: observables whose fold-balls stay disjoint still commute — locality survives arbitrary local kicks.

⚠️ Honest scope: kicked drives only. The light cone for the full exp(-(iτ)(H_free + V)) with a non-commuting non-diagonal V is genuine Lieb–Robinson (velocity bounds from commutator norms) — the promoted Stage-5 goal (specs/eft-stage4-plan.md, horizon note), not claimed here. Norms/topology: the scoped Matrix.Norms.L2Operator instances, used only internally (the statements are topology-free).

References

CV/LocalAlgebra.lean (CV-8 (i), the closure lemmas); CV/SupportSpreading.lean (CV-8 (ii)–(iv), heisenberg_supportedOn_union, heisenberg_eq_of_disjoint); specs/eft-stage4-plan.md (row CV-11); specs/future-work.md.

The local algebra, packaged

theorem CSD.CV.SupportedOn.zero {K N : ℕ} {S : Finset (Fin K)} : SupportedOn S 0

The zero matrix is supported on every region.

def CSD.CV.localSubmodule {K N : ℕ} (T : Finset (Fin K)) : Submodule ℂ (Matrix (FieldConfig K N) (FieldConfig K N) ℂ)

The local algebra as a ℂ-submodule.

Equations

• CSD.CV.localSubmodule T = { carrier := {A : Matrix (CSD.CV.FieldConfig K N) (CSD.CV.FieldConfig K N) ℂ | CSD.CV.SupportedOn T A}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def CSD.CV.localAlgebra {K N : ℕ} (T : Finset (Fin K)) : Subalgebra ℂ (Matrix (FieldConfig K N) (FieldConfig K N) ℂ)

The local algebra as a ℂ-subalgebra.

Equations

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

@[simp]

theorem CSD.CV.mem_localAlgebra {K N : ℕ} {T : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} : A ∈ localAlgebra T ↔ SupportedOn T A

Membership in the local algebra IS the support condition.

theorem CSD.CV.isClosed_localSubmodule {K N : ℕ} (T : Finset (Fin K)) : IsClosed ↑(localSubmodule T)

The local algebra is topologically closed — a subspace of a finite-dimensional matrix space.

Exp-closure

theorem CSD.CV.SupportedOn.pow {K N : ℕ} {T : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn T A) (n : ℕ) : SupportedOn T (A ^ n)

Powers of a supported matrix are supported.

theorem CSD.CV.SupportedOn.exp {K N : ℕ} {T : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn T A) : SupportedOn T (NormedSpace.exp A)

★ Exp-closure of the local algebra: the exponential of a T-supported matrix is T-supported. Every partial sum of the exponential series lives in the algebra; the limit stays by closedness.

Local kicks from arbitrary skew-Hermitian generators

theorem CSD.CV.expKick_unitary {K N : ℕ} {G : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : G.conjTranspose = -G) : NormedSpace.exp G ∈ Matrix.unitaryGroup (FieldConfig K N) ℂ

A skew-Hermitian generator exponentiates to a unitary (the generic unitarity core, at the FieldConfig index).

structure CSD.CV.KickData (K N : ℕ) : Type

A local kick: a unitary supported on an edge. The support field is all the light-cone argument consumes.

• edge : Fin K × Fin K

  The coupled edge.

• U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

  The kick unitary.

• supported : SupportedOn {self.edge.1, self.edge.2} ↑self.U

  The kick is supported on its edge.

noncomputable def CSD.CV.KickData.ofGenerator {K N : ℕ} (e : Fin K × Fin K) {G : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : G.conjTranspose = -G) (hsupp : SupportedOn {e.1, e.2} G) : KickData K N

Smart constructor: any skew-Hermitian edge-supported generator — hopping terms included — yields a local kick, by unitarity of the exponential and exp-closure of the local algebra.

Equations

• CSD.CV.KickData.ofGenerator e hG hsupp = { edge := e, U := ⟨NormedSpace.exp G, ⋯⟩, supported := ⋯ }

The kicked drive and its fold light cone

def CSD.CV.kickFoldStep {K : ℕ} (e : Fin K × Fin K) (R : Finset (Fin K)) : Finset (Fin K)

One kick's support growth: the edge is absorbed exactly when it touches the region.

Equations

• CSD.CV.kickFoldStep e R = if e.1 ∈ R ∨ e.2 ∈ R then insert e.1 (insert e.2 R) else R

def CSD.CV.kickFold {K : ℕ} (es : List (Fin K × Fin K)) (R : Finset (Fin K)) : Finset (Fin K)

The per-period support growth of a kick list (kicks may chain within a period; the fold records that honestly).

Equations

• CSD.CV.kickFold es R = List.foldl (fun (R : Finset (Fin K)) (e : Fin K × Fin K) => CSD.CV.kickFoldStep e R) R es

def CSD.CV.kickFoldBall {K : ℕ} (es : List (Fin K × Fin K)) (R : Finset (Fin K)) : ℕ → Finset (Fin K)

The n-period fold ball.

Equations

• CSD.CV.kickFoldBall es R 0 = R
• CSD.CV.kickFoldBall es R n.succ = CSD.CV.kickFold es (CSD.CV.kickFoldBall es R n)

noncomputable def CSD.CV.kickedStep {K N : ℕ} (τ : ℝ) (ks : List (KickData K N)) : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

The kicked drive: one free period followed by the kick list.

Equations

• CSD.CV.kickedStep τ ks = CSD.CV.freeFieldU K N τ * (List.map CSD.CV.KickData.U ks).prod

theorem CSD.CV.heisenberg_kick_supportedOn {K N : ℕ} {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (k : KickData K N) (hA : SupportedOn R A) : SupportedOn (kickFoldStep k.edge R) (heisenberg k.U A)

One kick spreads support at most onto its fold step.

theorem CSD.CV.heisenberg_kickList_supportedOn {K N : ℕ} {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (ks : List (KickData K N)) (hA : SupportedOn R A) : SupportedOn (kickFold (List.map KickData.edge ks) R) (heisenberg (List.map KickData.U ks).prod A)

A kick list spreads support at most onto its fold.

theorem CSD.CV.heisenberg_kickedStep_supportedOn {K N : ℕ} {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ : ℝ) (ks : List (KickData K N)) (hA : SupportedOn R A) : SupportedOn (kickFold (List.map KickData.edge ks) R) (heisenberg (kickedStep τ ks) A)

One kicked period spreads support at most onto the fold.

theorem CSD.CV.heisenberg_kickedStep_pow_supportedOn {K N : ℕ} {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ : ℝ) (ks : List (KickData K N)) (n : ℕ) (hA : SupportedOn R A) : SupportedOn (kickFoldBall (List.map KickData.edge ks) R n) (heisenberg (kickedStep τ ks ^ n) A)

★★ The non-diagonal light cone: after n periods of the kicked drive — free step plus ARBITRARY local kicks, hopping included — support lies inside the n-fold ball.

theorem CSD.CV.commute_heisenberg_kickedStep_pow {K N : ℕ} {R T : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ : ℝ) (ks : List (KickData K N)) (n : ℕ) (hRT : Disjoint (kickFoldBall (List.map KickData.edge ks) R n) (kickFoldBall (List.map KickData.edge ks) T n)) (hA : SupportedOn R A) (hB : SupportedOn T B) : heisenberg (kickedStep τ ks ^ n) A * heisenberg (kickedStep τ ks ^ n) B = heisenberg (kickedStep τ ks ^ n) B * heisenberg (kickedStep τ ks ^ n) A

★★ Locality outside the fold cones: observables whose fold-balls stay disjoint after n kicked periods still commute.