CV-17/CV-18: the Heisenberg flow and the linear Lieb-Robinson bound

Category: CV (continuous variables); the general lemmas are CSD-free (upstream-candidate(mathlib)).

Glossary: https://glossary.constraintsurfacedynamics.com/lieb-robinson-bound/ Plain-language, CSD-role and formal statements of the Lieb-Robinson bound, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Stage 5's first two bricks. Everything is stated for a skew-Hermitian generator S, which is -i H for Hermitian H, so that the propagators are unitary and the L2 operator norm sees them as isometries.

• heisenbergFlow S t A = exp (-t • S) * A * exp (t • S) — the observable after time t; norm_heisenbergFlow_le (conjugation by unitaries does not grow the norm), heisenbergFlow_zero.

• ★ hasDerivAt_heisenbergFlow — d/dt A(t) = [A(t), S] (CV-17).

• commutator_deriv_eq — the interaction-picture split. Writing S = S_X + T with S_X the part of the generator that commutes with the probe B, the commutator f(t) = [A(t), B] obeys f'(t) = [f(t), S_X] + [[A(t), T], B]. The first term is a pure conjugation and carries no growth; all the growth is in T, the part of the generator that couples across the cut. Proved by the Jacobi cancellation A·[S_X,B] - [S_X,B]·A = 0.

• ★★ norm_commutator_heisenbergFlow_le — the linear Lieb-Robinson bound: if [A, B] = 0 and S_X commutes with B, then ‖[A(t), B]‖ ≤ 4·|t|·‖T‖·‖A‖·‖B‖. Information cannot leave a region instantaneously: the commutator grows at most linearly in time, at a rate set by the coupling across the cut alone, not by the total energy.

• norm_commutator_field_le — the CV instantiation: disjointly supported observables of the field, with [A,B] = 0 supplied by CV-8's commute_of_disjointSupport.

• ★★ norm_commutator_gronwall_le (CV-19, partial) — the Gronwall bound: ‖[A(t),B]‖ ≤ gronwallBound 0 (2‖T‖) (2‖A‖‖[T,B]‖) t, which for ‖T‖ ≠ 0 reads (‖A‖‖[T,B]‖/‖T‖)(e^{2‖T‖t} − 1). Two things improve on the linear bound. The time dependence is exponential in ‖T‖t, which is the correct shape. And the prefactor is ‖[T,B]‖, the part of the coupling that actually reaches the probe, so commutator_eq_zero_of_coupling_commutes: a coupling commuting with B contributes exactly nothing, at any time.

• ★★ adIter_supportedOn_graphBall and commutator_adIter_eq_zero — the combinatorial half of the spatial cone. The Heisenberg flow is the exponential generating series of the nested commutators ad_S^k(A), and for a generator that is a sum of edge-supported terms those iterates stay inside the coupling graph's k-ball: a term whose edge misses the current region commutes with the observable and drops out, so k steps reach at most k edges. Consequently ad_S^k(A) commutes with B exactly whenever the k-ball has not yet reached B's region. That is what makes a Lieb-Robinson series start at the graph distance rather than at zero.

• ★★★ norm_commutator_spatial_le — the spatial bound: ‖[A(t), B]‖ ≤ 2‖A‖‖B‖·(2‖S‖|t|)^d for every d whose graph ball around A's region has not reached B's. Whenever 2‖S‖|t| < 1 this decays geometrically in the graph distance, so an observable at distance d is disturbed only after a time of order d/(2‖S‖): the propagation speed is bounded by the coupling strength. The two halves meet here. The Taylor remainder controls the flow to order d, and every discarded term commutes with B exactly, because k nested commutators reach at most k edges, so the whole commutator is carried by the remainder.

• ★★★ norm_commutator_spatial_factorial_le — the Lieb-Robinson bound with its factorial: ‖[A(t), B]‖ ≤ 2‖A‖‖B‖·(2‖S‖t)^d/d!, obtained by replacing the mean-value step in the remainder estimate with an integral one (norm_flowRemainder_le_factorial). Because of the factorial this decays in the graph distance at every time rather than only below 2‖S‖t = 1: at fixed t the bound falls faster than geometrically in d, which is the standard statement that the commutator is exponentially small outside an effective light cone.

⚠️ Honest scope. Both the geometric and factorial forms are proved; the factorial one is the sharper and is the textbook shape. No velocity constant is extracted or optimised: Lieb-Robinson velocities are famously not tight, and none is asserted here, so "light cone" refers to the decay in d at fixed t and not to an optimal speed. The interaction is a finite sum of edge-supported terms on a finite mode graph; nothing is claimed in the continuum (ApproxCCR.no_exact_finite_ccr stands).

References

Mathlib/Analysis/Matrix/DuhamelBound.lean (the mean-value pattern and the skew-generator lemmas); CV/SupportSpreading.lean (CV-8, the initial condition); specs/eft-stage5-plan.md (rows CV-17, CV-18); Lieb-Robinson (1972); Nachtergaele-Sims (2010).

CV-17: the Heisenberg flow

noncomputable def CSD.CV.heisenbergFlow {m : Type u_1} [Fintype m] [DecidableEq m] (S : Matrix m m ℂ) (t : ℝ) (A : Matrix m m ℂ) : Matrix m m ℂ

The Heisenberg flow generated by a skew-Hermitian S = -iH.

Equations

• CSD.CV.heisenbergFlow S t A = NormedSpace.exp (-t • S) * A * NormedSpace.exp (t • S)

@[simp]

theorem CSD.CV.heisenbergFlow_zero {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) : heisenbergFlow S 0 A = A

theorem CSD.CV.norm_heisenbergFlow_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S : Matrix m m ℂ} (hS : S.conjTranspose = -S) (t : ℝ) (A : Matrix m m ℂ) : ‖heisenbergFlow S t A‖ ≤ ‖A‖

Conjugation by the unitary propagators does not grow the norm.

theorem CSD.CV.hasDerivAt_heisenbergFlow {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) (t : ℝ) : HasDerivAt (fun (u : ℝ) => heisenbergFlow S u A) (heisenbergFlow S t A * S - S * heisenbergFlow S t A) t

★ CV-17: the Heisenberg flow solves d/dt A(t) = [A(t), S].

The interaction-picture split

theorem CSD.CV.commutator_deriv_eq {m : Type u_1} [Fintype m] [DecidableEq m] {S S_X T : Matrix m m ℂ} (A B : Matrix m m ℂ) (hsplit : S = S_X + T) (hcomm : S_X * B = B * S_X) (t : ℝ) : HasDerivAt (fun (u : ℝ) => heisenbergFlow S u A * B - B * heisenbergFlow S u A) ((heisenbergFlow S t A * B - B * heisenbergFlow S t A) * S_X - S_X * (heisenbergFlow S t A * B - B * heisenbergFlow S t A) + ((heisenbergFlow S t A * T - T * heisenbergFlow S t A) * B - B * (heisenbergFlow S t A * T - T * heisenbergFlow S t A))) t

The split. With S = S_X + T and S_X commuting with the probe B, the commutator [A(t), B] obeys f' = [f, S_X] + [[A(t), T], B]: the local part of the generator contributes only a conjugation, and all growth comes from T, the part that couples across the cut.

Conjugation invariance and the conjugated commutator

theorem CSD.CV.norm_conj_eq {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S_X : Matrix m m ℂ} (hSX : S_X.conjTranspose = -S_X) (t : ℝ) (M : Matrix m m ℂ) : ‖NormedSpace.exp (t • S_X) * M * NormedSpace.exp (-t • S_X)‖ = ‖M‖

Conjugation by the unitaries generated by a skew-Hermitian S_X preserves the L2 operator norm.

noncomputable def CSD.CV.conjComm {m : Type u_1} [Fintype m] [DecidableEq m] (S S_X A B : Matrix m m ℂ) (t : ℝ) : Matrix m m ℂ

The conjugated commutator: the commutator viewed in the frame that rotates with the local part of the generator. Its derivative has no conjugation term, which is what makes the estimates work.

Equations

• CSD.CV.conjComm S S_X A B t = NormedSpace.exp (t • S_X) * (CSD.CV.heisenbergFlow S t A * B - B * CSD.CV.heisenbergFlow S t A) * NormedSpace.exp (-t • S_X)

theorem CSD.CV.norm_conjComm {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S_X : Matrix m m ℂ} (hSX : S_X.conjTranspose = -S_X) (S A B : Matrix m m ℂ) (t : ℝ) : ‖conjComm S S_X A B t‖ = ‖heisenbergFlow S t A * B - B * heisenbergFlow S t A‖

The conjugated commutator has the same norm as the commutator.

@[simp]

theorem CSD.CV.conjComm_zero {m : Type u_1} [Fintype m] [DecidableEq m] (S S_X A B : Matrix m m ℂ) : conjComm S S_X A B 0 = A * B - B * A

theorem CSD.CV.hasDerivAt_conjComm {m : Type u_1} [Fintype m] [DecidableEq m] {S S_X T : Matrix m m ℂ} (A B : Matrix m m ℂ) (hsplit : S = S_X + T) (hcomm : S_X * B = B * S_X) (s : ℝ) : HasDerivAt (conjComm S S_X A B) (NormedSpace.exp (s • S_X) * ((heisenbergFlow S s A * T - T * heisenbergFlow S s A) * B - B * (heisenbergFlow S s A * T - T * heisenbergFlow S s A)) * NormedSpace.exp (-s • S_X)) s

The derivative of the conjugated commutator is the leakage term, with the local part of the generator gone.

theorem CSD.CV.norm_leak_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S T A B : Matrix m m ℂ} (hS : S.conjTranspose = -S) (s : ℝ) : ‖(heisenbergFlow S s A * T - T * heisenbergFlow S s A) * B - B * (heisenbergFlow S s A * T - T * heisenbergFlow S s A)‖ ≤ 4 * ‖T‖ * ‖A‖ * ‖B‖

The leakage term, bounded crudely.

CV-18: the linear bound

theorem CSD.CV.norm_commutator_heisenbergFlow_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S S_X T A B : Matrix m m ℂ} (hS : S.conjTranspose = -S) (hSX : S_X.conjTranspose = -S_X) (hsplit : S = S_X + T) (hcomm : S_X * B = B * S_X) (hAB : A * B = B * A) (t : ℝ) : ‖heisenbergFlow S t A * B - B * heisenbergFlow S t A‖ ≤ 4 * |t| * ‖T‖ * ‖A‖ * ‖B‖

★★ CV-18, the linear Lieb-Robinson bound. If the observables commute at time zero and the local part S_X of the generator commutes with the probe B, then the commutator grows at most linearly in time, at a rate set by T (the part of the generator coupling across the cut) alone: ‖[A(t), B]‖ ≤ 4·|t|·‖T‖·‖A‖·‖B‖. Information cannot leave a region instantaneously.

CV-19 (partial): the Gronwall bound

theorem CSD.CV.leak_jacobi {m : Type u_1} [Fintype m] [DecidableEq m] (F T B : Matrix m m ℂ) : (F * T - T * F) * B - B * (F * T - T * F) = (F * B - B * F) * T - T * (F * B - B * F) + (F * (T * B - B * T) - (T * B - B * T) * F)

The Jacobi re-split of the leakage term. The double commutator with the coupling splits into a term proportional to the commutator being estimated and a term proportional to [T, B], the part of the coupling that actually reaches the probe.

theorem CSD.CV.norm_leak_gronwall_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S T A B : Matrix m m ℂ} (hS : S.conjTranspose = -S) (s : ℝ) : ‖(heisenbergFlow S s A * T - T * heisenbergFlow S s A) * B - B * (heisenbergFlow S s A * T - T * heisenbergFlow S s A)‖ ≤ 2 * ‖T‖ * ‖heisenbergFlow S s A * B - B * heisenbergFlow S s A‖ + 2 * ‖A‖ * ‖T * B - B * T‖

The leakage term, bounded in Gronwall shape: proportional to the current commutator, plus a source proportional to ‖[T, B]‖.

theorem CSD.CV.norm_commutator_gronwall_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S S_X T A B : Matrix m m ℂ} (hS : S.conjTranspose = -S) (hSX : S_X.conjTranspose = -S_X) (hsplit : S = S_X + T) (hcomm : S_X * B = B * S_X) (hAB : A * B = B * A) {t : ℝ} (ht : 0 ≤ t) : ‖heisenbergFlow S t A * B - B * heisenbergFlow S t A‖ ≤ gronwallBound 0 (2 * ‖T‖) (2 * ‖A‖ * ‖T * B - B * T‖) t

★★ The Gronwall (exponential-in-time) Lieb-Robinson bound. The commutator obeys ‖[A(t), B]‖ ≤ gronwallBound 0 (2‖T‖) (2‖A‖‖[T,B]‖) t, which for ‖T‖ ≠ 0 is (‖A‖‖[T,B]‖/‖T‖)·(e^{2‖T‖t} − 1).

Two things are sharper here than in CV-18. The growth is exponential in ‖T‖t rather than linear, which is the correct time dependence. More importantly the prefactor is ‖[T, B]‖, the part of the coupling that actually reaches the probe: if the coupling term commutes with B, the bound is identically zero for all time. That vanishing is the seed of a spatial light cone; converting it into one requires the iteration over chains of interaction terms, which is not done here.

theorem CSD.CV.commutator_eq_zero_of_coupling_commutes {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S S_X T A B : Matrix m m ℂ} (hS : S.conjTranspose = -S) (hSX : S_X.conjTranspose = -S_X) (hsplit : S = S_X + T) (hcomm : S_X * B = B * S_X) (hTB : T * B = B * T) (hAB : A * B = B * A) {t : ℝ} (ht : 0 ≤ t) : heisenbergFlow S t A * B - B * heisenbergFlow S t A = 0

The vanishing case, stated on its own: a coupling term that commutes with the probe contributes nothing, at any time.

The adjoint action

def CSD.CV.adOne {n : Type u_2} [Fintype n] [DecidableEq n] (G A : Matrix n n ℂ) : Matrix n n ℂ

One step of the adjoint action: ad_G(A) = [G, A].

Equations

• CSD.CV.adOne G A = G * A - A * G

def CSD.CV.adIter {n : Type u_2} [Fintype n] [DecidableEq n] (S : Matrix n n ℂ) : ℕ → Matrix n n ℂ → Matrix n n ℂ

The k-fold adjoint action ad_S^k. The Heisenberg flow is its exponential generating series, which is why the support of these iterates controls the spatial reach of the dynamics.

Equations

• CSD.CV.adIter S 0 x✝ = x✝
• CSD.CV.adIter S k.succ x✝ = CSD.CV.adOne S (CSD.CV.adIter S k x✝)

@[simp]

theorem CSD.CV.adIter_zero {n : Type u_2} [Fintype n] [DecidableEq n] (S A : Matrix n n ℂ) : adIter S 0 A = A

@[simp]

theorem CSD.CV.adIter_succ {n : Type u_2} [Fintype n] [DecidableEq n] (S A : Matrix n n ℂ) (k : ℕ) : adIter S (k + 1) A = adOne S (adIter S k A)

theorem CSD.CV.adOne_sum {n : Type u_2} {ι : Type u_3} [Fintype n] [DecidableEq n] (E : Finset ι) (G : ι → Matrix n n ℂ) (A : Matrix n n ℂ) : adOne (∑ e ∈ E, G e) A = ∑ e ∈ E, adOne (G e) A

The adjoint action is linear in the generator.

The Taylor remainder of the flow

noncomputable def CSD.CV.flowCoef (t : ℝ) (k : ℕ) : ℝ

The Taylor coefficients of the Heisenberg flow, as real scalars.

Equations

• CSD.CV.flowCoef t k = (-1) ^ k / ↑k.factorial * t ^ k

@[simp]

theorem CSD.CV.flowCoef_zero (t : ℝ) : flowCoef t 0 = 1

noncomputable def CSD.CV.flowRemainder {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) (k : ℕ) (t : ℝ) : Matrix m m ℂ

The Taylor remainder of the flow after k terms of its adjoint series.

Equations

• CSD.CV.flowRemainder S A k t = CSD.CV.heisenbergFlow S t A - ∑ j ∈ Finset.range k, CSD.CV.flowCoef t j • CSD.CV.adIter S j A

@[simp]

theorem CSD.CV.flowRemainder_zero_terms {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) (t : ℝ) : flowRemainder S A 0 t = heisenbergFlow S t A

theorem CSD.CV.adOne_smul {m : Type u_1} [Fintype m] [DecidableEq m] (S : Matrix m m ℂ) (c : ℝ) (A : Matrix m m ℂ) : adOne S (c • A) = c • adOne S A

The adjoint action commutes with real scalars in its second argument.

theorem CSD.CV.adOne_sub {m : Type u_1} [Fintype m] [DecidableEq m] (S X Y : Matrix m m ℂ) : adOne S (X - Y) = adOne S X - adOne S Y

theorem CSD.CV.adOne_sum_range {m : Type u_1} [Fintype m] [DecidableEq m] (S : Matrix m m ℂ) (k : ℕ) (f : ℕ → Matrix m m ℂ) : adOne S (∑ j ∈ Finset.range k, f j) = ∑ j ∈ Finset.range k, adOne S (f j)

theorem CSD.CV.norm_adIter_le {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) (k : ℕ) : ‖adIter S k A‖ ≤ (2 * ‖S‖) ^ k * ‖A‖

The norm of a nested commutator grows by at most 2‖S‖ per step.

theorem CSD.CV.hasDerivAt_flowCoef (t : ℝ) (j : ℕ) : HasDerivAt (fun (u : ℝ) => flowCoef u (j + 1)) (-flowCoef t j) t

Each Taylor coefficient differentiates into its predecessor.

theorem CSD.CV.hasDerivAt_flowRemainder {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) (k : ℕ) (t : ℝ) : HasDerivAt (flowRemainder S A (k + 1)) (-adOne S (flowRemainder S A k t)) t

The remainder solves the same linear equation the flow does: the Taylor terms differentiate into one another and cancel, leaving d/dt Rₖ₊₁(t) = -ad_S(Rₖ(t)).

theorem CSD.CV.norm_flowRemainder_le {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S : Matrix m m ℂ} (hS : S.conjTranspose = -S) (A : Matrix m m ℂ) (k : ℕ) (t : ℝ) : ‖flowRemainder S A k t‖ ≤ (2 * ‖S‖ * |t|) ^ k * ‖A‖

★★ The Taylor remainder is small: ‖Rₖ(t)‖ ≤ (2‖S‖|t|)ᵏ‖A‖, so the flow is approximated by the first k terms of its adjoint series to that order.

The factorial remainder bound

theorem CSD.CV.exists_hasDerivAt_flowRemainder {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) (k : ℕ) (t : ℝ) : ∃ (v : Matrix m m ℂ), HasDerivAt (flowRemainder S A k) v t

The remainder is differentiable at every time, hence continuous.

theorem CSD.CV.continuous_flowRemainder {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) (k : ℕ) : Continuous (flowRemainder S A k)

theorem CSD.CV.continuous_adOne_flowRemainder {m : Type u_1} [Fintype m] [DecidableEq m] (S A : Matrix m m ℂ) (k : ℕ) : Continuous fun (s : ℝ) => -adOne S (flowRemainder S A k s)

theorem CSD.CV.norm_flowRemainder_le_factorial {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] {S : Matrix m m ℂ} (hS : S.conjTranspose = -S) (A : Matrix m m ℂ) (k : ℕ) {t : ℝ} (ht : 0 ≤ t) : ‖flowRemainder S A k t‖ ≤ (2 * ‖S‖ * t) ^ k / ↑k.factorial * ‖A‖

★★★ The factorial remainder bound. Replacing the mean-value step by an integral estimate sharpens norm_flowRemainder_le to ‖Rₖ(t)‖ ≤ (2‖S‖t)ᵏ/k!·‖A‖. The factorial is what makes the spatial bound decay at every time rather than only below 2‖S‖t = 1.

Toward the spatial cone: nested commutators stay in the ball

theorem CSD.CV.adOne_supportedOn_graphNeighborhood {K N : ℕ} {E : Finset (Fin K × Fin K)} {G : Fin K × Fin K → Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : ∀ e ∈ E, SupportedOn {e.1, e.2} (G e)) {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) : SupportedOn (graphNeighborhood E R) (adOne (∑ e ∈ E, G e) A)

One adjoint step grows support by at most one graph edge. A term whose edge misses the current region commutes with the observable and contributes nothing; a term whose edge touches it contributes inside the one-step neighbourhood.

theorem CSD.CV.adIter_supportedOn_graphBall {K N : ℕ} {E : Finset (Fin K × Fin K)} {G : Fin K × Fin K → Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : ∀ e ∈ E, SupportedOn {e.1, e.2} (G e)) {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) (n : ℕ) : SupportedOn (graphBall E R n) (adIter (∑ e ∈ E, G e) n A)

★★ The iterated adjoint action stays inside the graph ball. After n nested commutators with a sum of edge-supported generators, the observable is still supported within the coupling graph's n-ball. This is the combinatorial heart of a spatial light cone: it is the statement that n steps of the dynamics reach at most n edges.

theorem CSD.CV.commutator_adIter_eq_zero {K N : ℕ} {E : Finset (Fin K × Fin K)} {G : Fin K × Fin K → Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : ∀ e ∈ E, SupportedOn {e.1, e.2} (G e)) {R Y : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) (hB : SupportedOn Y B) {n : ℕ} (hcone : Disjoint (graphBall E R n) Y) : adIter (∑ e ∈ E, G e) n A * B = B * adIter (∑ e ∈ E, G e) n A

★★ Exact vanishing below the light cone. If the coupling graph's n-ball around A's region has not yet reached B's region, the n-th nested commutator commutes with B exactly. Since the Heisenberg flow is the exponential generating series of these iterates, this is what makes a Lieb-Robinson series start at the graph distance rather than at zero.

The spatial Lieb-Robinson bound

theorem CSD.CV.norm_commutator_spatial_le {K N : ℕ} [NeZero N] {E : Finset (Fin K × Fin K)} {G : Fin K × Fin K → Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : ∀ e ∈ E, SupportedOn {e.1, e.2} (G e)) (hS : (∑ e ∈ E, G e).conjTranspose = -∑ e ∈ E, G e) {R Y : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) (hB : SupportedOn Y B) {d : ℕ} (hcone : Disjoint (graphBall E R d) Y) (t : ℝ) : ‖heisenbergFlow (∑ e ∈ E, G e) t A * B - B * heisenbergFlow (∑ e ∈ E, G e) t A‖ ≤ 2 * (2 * ‖∑ e ∈ E, G e‖ * |t|) ^ d * ‖A‖ * ‖B‖

★★★ The spatial Lieb-Robinson bound. For observables supported on regions R and Y of the coupling graph, and a skew-Hermitian generator that is a sum of edge-supported terms, the commutator after time t is bounded by 2‖A‖‖B‖·(2‖S‖|t|)^d for every d whose graph ball around R has not yet reached Y.

This is a light cone. Whenever 2‖S‖|t| < 1, the bound decays geometrically in the graph distance, so an observable at distance d feels a disturbance only after a time of order d / (2‖S‖): the propagation speed is bounded by the coupling strength.

The proof combines the two halves. The Taylor remainder controls the flow to order d (norm_flowRemainder_le), and every discarded term commutes with B exactly, because k nested commutators reach at most k graph edges (commutator_adIter_eq_zero). So the entire commutator is carried by the remainder alone.

theorem CSD.CV.norm_commutator_spatial_factorial_le {K N : ℕ} [NeZero N] {E : Finset (Fin K × Fin K)} {G : Fin K × Fin K → Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : ∀ e ∈ E, SupportedOn {e.1, e.2} (G e)) (hS : (∑ e ∈ E, G e).conjTranspose = -∑ e ∈ E, G e) {R Y : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) (hB : SupportedOn Y B) {d : ℕ} (hcone : Disjoint (graphBall E R d) Y) {t : ℝ} (ht : 0 ≤ t) : ‖heisenbergFlow (∑ e ∈ E, G e) t A * B - B * heisenbergFlow (∑ e ∈ E, G e) t A‖ ≤ 2 * ((2 * ‖∑ e ∈ E, G e‖ * t) ^ d / ↑d.factorial) * ‖A‖ * ‖B‖

★★★ The Lieb-Robinson bound. Sharpening the geometric bound with the factorial remainder estimate: ‖[A(t), B]‖ ≤ 2‖A‖‖B‖·(2‖S‖t)^d/d! for every d whose graph ball around A's region has not reached B's.

Because of the factorial this decays in the graph distance at every time, not only for 2‖S‖t < 1: at fixed t the bound falls faster than geometrically in d, which is the standard Lieb-Robinson statement that the commutator is exponentially small outside an effective light cone.

The CV instantiation

theorem CSD.CV.norm_commutator_field_le {K N : ℕ} [NeZero N] {S S_X T : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} {R Y : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hS : S.conjTranspose = -S) (hSX : S_X.conjTranspose = -S_X) (hsplit : S = S_X + T) (hcomm : S_X * B = B * S_X) (hRY : Disjoint R Y) (hA : SupportedOn R A) (hB : SupportedOn Y B) (t : ℝ) : ‖heisenbergFlow S t A * B - B * heisenbergFlow S t A‖ ≤ 4 * |t| * ‖T‖ * ‖A‖ * ‖B‖

★ On the field: for observables supported on disjoint mode sets, the commutator after time t is bounded by the cut coupling alone. The zero-time commutation hypothesis is supplied by CV-8's commute_of_disjointSupport, so only the generator split has to be provided.

CV-20 (Stage 6): the velocity, made explicit

theorem CSD.CV.pow_pow_le_exp_mul_factorial (d : ℕ) : ↑d ^ d ≤ Real.exp ↑d * ↑d.factorial

The exponential-series lower bound in the form the velocity extraction needs: d^d ≤ e^d · d! (one term of the series for exp d).

theorem CSD.CV.pow_div_factorial_le_exp_neg {x : ℝ} (hx : 0 ≤ x) {d : ℕ} (h : Real.exp 1 ^ 2 * x ≤ ↑d) : x ^ d / ↑d.factorial ≤ Real.exp (-↑d)

Outside x ≤ d/e² the series term dies exponentially: x^d/d! ≤ e^{−d}. The arithmetic engine of the velocity bound.

theorem CSD.CV.norm_commutator_velocity_le {K N : ℕ} [NeZero N] {E : Finset (Fin K × Fin K)} {G : Fin K × Fin K → Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : ∀ e ∈ E, SupportedOn {e.1, e.2} (G e)) (hS : (∑ e ∈ E, G e).conjTranspose = -∑ e ∈ E, G e) {R Y : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) (hB : SupportedOn Y B) {d : ℕ} (hcone : Disjoint (graphBall E R d) Y) {t : ℝ} (ht : 0 ≤ t) (hv : Real.exp 1 ^ 2 * (2 * ‖∑ e ∈ E, G e‖ * t) ≤ ↑d) : ‖heisenbergFlow (∑ e ∈ E, G e) t A * B - B * heisenbergFlow (∑ e ∈ E, G e) t A‖ ≤ 2 * Real.exp (-↑d) * ‖A‖ * ‖B‖

★★★ The Lieb–Robinson velocity (CV-20, Stage 6): outside the cone v·t ≤ d with v := 2e²·‖S‖, the commutator is exponentially small in the graph distance — ‖[A(t), B]‖ ≤ 2‖A‖‖B‖·e^{−d}. The Stage-5 factorial bound with the velocity constant made explicit: information propagates through the coupling graph no faster than 2e²‖S‖ edges per unit time, up to exponentially small tails. No optimality of the constant is claimed.