CV-8 (ii)–(iv): support spreading and the coupling-graph light cone

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

CV-6 proved the free field never spreads support. This module bounds what an interaction can do:

• phaseDiagU_supportedOn — a diagonal phase depending only on the modes in T is a T-supported unitary.
• heisenberg_supportedOn_union — conjugation by ANY T-supported unitary maps the S-algebra into the S ∪ T-algebra (three lines from the LocalAlgebra closure).
• heisenberg_eq_of_disjoint — a coupling disjoint from the support acts trivially: support only grows into modes the interaction actually couples.
• heisenberg_addGraphPhase_supportedOn — the sharp one-period bound for the diagonal interacting drive: a mode-additive-plus-edge-sum phase spreads S at most onto graphNeighborhood E S (the conjugating phase difference collapses to the touched edges, graph_sum_sub_of_agree).
• ★★ heisenberg_graphInteractingU_pow_supportedOn — the light cone: after n periods of the interacting drive, support lies inside the coupling graph's n-ball graphBall E S n — information propagates at most one graph edge per period. With commute_heisenberg_graphInteractingU_pow: observables whose n-balls are still disjoint — outside each other's light cones — still commute.
• spreadKick_not_supportedOn — non-vacuity (the converse of CV-6): at K = N = 2 a concrete pair kick moves modeOp 0 off the single-mode algebra — the evolved entries at spectator occupations 0 and 1 are 1 and −1. Interaction genuinely spreads; the light cone is a bound on a real phenomenon, not a vacuous one.

This retires CV-6's open boundary: interacting-drive spreading is now a theorem with a bound, not an unclaimed scope. The norm pricing landed as CV-9 (CV/InteractionPrice.lean, covering non-diagonal perturbations too), and the non-diagonal KICKED cone landed as CV-11 (CV/LocalAlgebraClosed.lean, the exp-closure route delivered); what remains open is the full-exponential cone — Lieb–Robinson velocity bounds, the promoted Stage-5 headline (specs/eft-stage4-plan.md, horizon note).

References

CV/LocalAlgebra.lean (CV-8 (i)); CV/DynamicalLocality.lean (CV-6, the free case); CV/Interaction.lean (CV-7, interactingU); specs/cv-stage3-plan.md §3b; specs/future-work.md (row CV-8). Haag, Local Quantum Physics (1992); Lieb–Robinson (1972) for the continuum-flavoured analogue of the light cone.

Conjugation by a supported unitary

theorem CSD.CV.phaseDiagU_supportedOn {K N : ℕ} {T : Finset (Fin K)} {f : FieldConfig K N → ℝ} (hf : ∀ (c c' : FieldConfig K N), (∀ k ∈ T, c k = c' k) → f c = f c') : SupportedOn T ↑(phaseDiagU f)

A diagonal phase depending only on the modes in T is a T-supported unitary.

theorem CSD.CV.heisenberg_supportedOn_union {K N : ℕ} {S T : Finset (Fin K)} {U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hU : SupportedOn T ↑U) (hA : SupportedOn S A) : SupportedOn (S ∪ T) (heisenberg U A)

Conjugation by a T-supported unitary maps the S-algebra into the S ∪ T-algebra — from the LocalAlgebra closure alone.

theorem CSD.CV.heisenberg_eq_of_disjoint {K N : ℕ} {S T : Finset (Fin K)} (hST : Disjoint S T) {U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hU : SupportedOn T ↑U) (hA : SupportedOn S A) : heisenberg U A = A

A coupling disjoint from the support acts trivially: support only grows into modes the interaction actually couples.

The coupling graph

def CSD.CV.graphNeighborhood {K : ℕ} (E : Finset (Fin K × Fin K)) (R : Finset (Fin K)) : Finset (Fin K)

The one-step neighbourhood: R together with both endpoints of every edge that touches R.

Equations

• CSD.CV.graphNeighborhood E R = R ∪ {e ∈ E | e.1 ∈ R ∨ e.2 ∈ R}.biUnion fun (e : Fin K × Fin K) => {e.1, e.2}

theorem CSD.CV.subset_graphNeighborhood {K : ℕ} (E : Finset (Fin K × Fin K)) (R : Finset (Fin K)) : R ⊆ graphNeighborhood E R

theorem CSD.CV.mem_graphNeighborhood_fst {K : ℕ} {E : Finset (Fin K × Fin K)} {R : Finset (Fin K)} {e : Fin K × Fin K} (he : e ∈ E) (ht : e.1 ∈ R ∨ e.2 ∈ R) : e.1 ∈ graphNeighborhood E R

theorem CSD.CV.mem_graphNeighborhood_snd {K : ℕ} {E : Finset (Fin K × Fin K)} {R : Finset (Fin K)} {e : Fin K × Fin K} (he : e ∈ E) (ht : e.1 ∈ R ∨ e.2 ∈ R) : e.2 ∈ graphNeighborhood E R

def CSD.CV.graphBall {K : ℕ} (E : Finset (Fin K × Fin K)) (R : Finset (Fin K)) : ℕ → Finset (Fin K)

The n-ball: n applications of the one-step neighbourhood — the light cone of R after n periods.

Equations

• CSD.CV.graphBall E R 0 = R
• CSD.CV.graphBall E R n.succ = CSD.CV.graphNeighborhood E (CSD.CV.graphBall E R n)

@[simp]

theorem CSD.CV.graphBall_zero {K : ℕ} (E : Finset (Fin K × Fin K)) (R : Finset (Fin K)) : graphBall E R 0 = R

@[simp]

theorem CSD.CV.graphBall_succ {K : ℕ} (E : Finset (Fin K × Fin K)) (R : Finset (Fin K)) (n : ℕ) : graphBall E R (n + 1) = graphNeighborhood E (graphBall E R n)

theorem CSD.CV.graphBall_mono {K : ℕ} (E : Finset (Fin K × Fin K)) (R : Finset (Fin K)) {i j : ℕ} (hij : i ≤ j) : graphBall E R i ⊆ graphBall E R j

The balls grow with the period count.

The phase-difference collapse for edge sums

theorem CSD.CV.graph_sum_sub_of_agree {K N : ℕ} {R : Finset (Fin K)} (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) {x y : FieldConfig K N} (hxy : ∀ k ∉ R, x k = y k) : ∑ e ∈ E, g e (y e.1) (y e.2) - ∑ e ∈ E, g e (x e.1) (x e.2) = ∑ e ∈ E with e.1 ∈ R ∨ e.2 ∈ R, (g e (y e.1) (y e.2) - g e (x e.1) (x e.2))

Off-R agreement collapses an edge-sum difference to the edges that touch R.

theorem CSD.CV.star_exp_phase_mul (a b : ℝ) : star (Complex.exp (-(Complex.I * ↑a))) * Complex.exp (-(Complex.I * ↑b)) = Complex.exp (-(Complex.I * ↑(b - a)))

The conjugating phase pair of any real phase: e^{+ia}·e^{-ib} = e^{-i(b−a)}.

theorem CSD.CV.addGraph_phase_diff_eq {K N : ℕ} {R : Finset (Fin K)} (h : Fin K → Fin N → ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) {x y x' y' : FieldConfig K N} (hxy : ∀ k ∉ R, x k = y k) (hxy' : ∀ k ∉ R, x' k = y' k) (hxx' : ∀ k ∈ graphNeighborhood E R, x k = x' k) (hyy' : ∀ k ∈ graphNeighborhood E R, y k = y' k) : ∑ k : Fin K, h k (y k) + ∑ e ∈ E, g e (y e.1) (y e.2) - (∑ k : Fin K, h k (x k) + ∑ e ∈ E, g e (x e.1) (x e.2)) = ∑ k : Fin K, h k (y' k) + ∑ e ∈ E, g e (y' e.1) (y' e.2) - (∑ k : Fin K, h k (x' k) + ∑ e ∈ E, g e (x' e.1) (x' e.2))

The phase difference of a mode-additive-plus-edge-sum phase depends only on the modes of graphNeighborhood E R, for configuration pairs agreeing off R.

The one-period spreading bound

theorem CSD.CV.heisenberg_addGraphPhase_supportedOn {K N : ℕ} {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (h : Fin K → Fin N → ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) (hA : SupportedOn R A) : SupportedOn (graphNeighborhood E R) (heisenberg (phaseDiagU fun (c : FieldConfig K N) => ∑ k : Fin K, h k (c k) + ∑ e ∈ E, g e (c e.1) (c e.2)) A)

One period of a diagonal interacting drive spreads support at most onto the one-step neighbourhood: for a phase = mode-additive part + edge sum over E, conjugation maps the R-algebra into the graphNeighborhood E R-algebra.

The interacting drive and its light cone

def CSD.CV.graphPotential {K N : ℕ} (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) : FieldConfig K N → ℝ

The graph potential: a sum of pair couplings over the edges of E.

Equations

• CSD.CV.graphPotential E g c = ∑ e ∈ E, g e (c e.1) (c e.2)

noncomputable def CSD.CV.graphInteractingU (K N : ℕ) (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

The graph-interacting drive: the CV-7 interacting step at the graph potential — the free field plus pair couplings along the edges of E.

Equations

• CSD.CV.graphInteractingU K N τ lam E g = CSD.CV.interactingU K N τ lam (CSD.CV.graphPotential E g)

theorem CSD.CV.heisenberg_graphInteractingU_supportedOn {K N : ℕ} {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) (hA : SupportedOn R A) : SupportedOn (graphNeighborhood E R) (heisenberg (graphInteractingU K N τ lam E g) A)

One interacting period spreads support at most one graph neighbourhood.

theorem CSD.CV.heisenberg_graphInteractingU_pow_supportedOn {K N : ℕ} {R : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) (n : ℕ) (hA : SupportedOn R A) : SupportedOn (graphBall E R n) (heisenberg (graphInteractingU K N τ lam E g ^ n) A)

★★ The light cone: after n periods of the interacting drive, support lies inside the coupling graph's n-ball — information propagates at most one graph edge per period.

theorem CSD.CV.commute_heisenberg_graphInteractingU_pow {K N : ℕ} {R T : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) (n : ℕ) (hRT : Disjoint (graphBall E R n) (graphBall E T n)) (hA : SupportedOn R A) (hB : SupportedOn T B) : heisenberg (graphInteractingU K N τ lam E g ^ n) A * heisenberg (graphInteractingU K N τ lam E g ^ n) B = heisenberg (graphInteractingU K N τ lam E g ^ n) B * heisenberg (graphInteractingU K N τ lam E g ^ n) A

★★ Locality outside the light cones: observables whose n-balls are still disjoint — not yet causally connected through the coupling graph — still commute after n interacting periods.

Non-vacuity: interaction genuinely spreads

noncomputable def CSD.CV.spreadPotential : FieldConfig 2 2 → ℝ

The witness pair potential at K = N = 2: phase π exactly when both modes are excited.

Equations

• CSD.CV.spreadPotential c = if c 0 = 1 ∧ c 1 = 1 then Real.pi else 0

noncomputable def CSD.CV.spreadKick : ↥(Matrix.unitaryGroup (FieldConfig 2 2) ℂ)

The witness kick: the diagonal unitary of spreadPotential.

Equations

• CSD.CV.spreadKick = CSD.CV.phaseDiagU CSD.CV.spreadPotential

noncomputable def CSD.CV.raiseMat : Matrix (Fin 2) (Fin 2) ℂ

The witness single-mode operator: the raising matrix |1⟩⟨0|-style !![0, 1; 0, 0].

Equations

• CSD.CV.raiseMat = !![0, 1; 0, 0]

theorem CSD.CV.spreadKick_not_supportedOn : ¬SupportedOn {0} (heisenberg spreadKick (modeOp 0 raiseMat))

★ Non-vacuity — the converse of CV-6: the pair kick moves the single-mode operator OFF the single-mode algebra. The evolved entries at spectator occupation 0 and 1 are 1 and −1, so indep fails: interaction genuinely spreads support, and the light cone bounds a real phenomenon.