CV/ModeLocality: commuting algebras of disjoint mode sets (EFT Stage 2b)

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

The locality half of EFT Stage 2, stated at the finite cutoff where it is actually true.

An operator on the field is supported on a set S of modes (SupportedOn) when it (i) does not move the modes outside S and (ii) has entries that do not depend on those spectator modes. The headline is the Haag–Kastler kinematic locality axiom:

commute_of_disjointSupport — S ∩ T = ∅ ⟹ A * B = B * A

for A supported on S and B supported on T. Observables of disjoint mode sets commute, so they are jointly measurable and the record layer can assign them outcomes simultaneously.

A non-vacuous witness is supplied rather than assumed: modeOp k₀ a acts as the single-mode matrix a on mode k₀ and as the identity elsewhere, is provably SupportedOn {k₀} (modeOp_supportedOn), and two such at distinct modes commute (commute_modeOp) for every pair of single-mode matrices.

What "locality" does and does not mean here

The theorem is about disjoint tensor factors. Under the position-space reading — the K modes are lattice sites, as seeded by CV/Position.lean — this is genuine spatial locality: observables of disjoint regions of the lattice commute. Under the momentum-space reading (the p k of CV/Dispersion.lean) the modes are delocalised, and mode-disjointness is not spatial separation; the statement is then subsystem locality, not microcausality.

Continuum microcausality — [φ(x), φ(y)] = 0 for spacelike-separated x, y — is NOT proved here, and does not hold exactly at a finite cutoff. It needs the continuum limit, which the EFT posture of this chain deliberately defers (CV/ApproxCCR.lean no_exact_finite_ccr: no finite model satisfies the CCR exactly). What is delivered is the finite-cutoff statement that survives that limit as the locality axiom: commuting algebras for disjoint regions. Calling this microcausality would overstate it; it is its kinematic core.

References

CV/Dispersion.lean (Stage 2a, the dispersion relation); CV/FieldModes.lean (Stage 1, the mode product); CV/Position.lean (the spatial lattice, under which mode-disjointness reads as spatial disjointness); CV/ApproxCCR.lean (no_exact_finite_ccr, why the continuum is deferred); SigmaLayer/Measurement.lean (the record layer that commuting observables let act jointly); specs/BACKLOG.md (the CV-chain row); specs/future-work.md. Haag, Local Quantum Physics (1992); Haag–Kastler (1964).

Support on a set of modes

structure CSD.CV.SupportedOn {K N : ℕ} (S : Finset (Fin K)) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : Prop

An operator is supported on the mode set S when it acts only on those modes: it does not move the spectator modes outside S (offDiag), and its entries do not depend on them (indep). This is the finite-cutoff form of "an observable localised in a region".

• offDiag {c d : FieldConfig K N} {k : Fin K} : k ∉ S → c k ≠ d k → A c d = 0

  A does not move the modes outside S: an entry between configurations that differ on a spectator mode vanishes.

• indep {c d c' d' : FieldConfig K N} : (∀ k ∈ S, c k = c' k) → (∀ k ∈ S, d k = d' k) → (∀ k ∉ S, c k = d k) → (∀ k ∉ S, c' k = d' k) → A c d = A c' d'

  A's entries depend only on the modes in S: two entries whose S-components agree, and whose spectator components are unmoved, are equal.

Locality: disjoint supports commute

theorem CSD.CV.commute_of_disjointSupport {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) : A * B = B * A

The Haag–Kastler locality axiom at a finite cutoff. Operators supported on disjoint mode sets commute — so observables of disjoint regions are jointly measurable, and the record layer can assign them outcomes simultaneously.

The proof is the uniqueness of the intermediate configuration. If c and d differ on a mode outside S ∪ T, then every term of both matrix products vanishes. Otherwise exactly one intermediate configuration survives in each product — e₁ (d on S, c off S) in A·B and e₂ (c on S, d off S) in B·A — and the two surviving products are the same two numbers in the other order, by indep.

A non-vacuous witness: single-mode operators

noncomputable def CSD.CV.modeOp {K N : ℕ} (k₀ : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The operator acting as the single-mode matrix a on mode k₀ and as the identity on every other mode.

Equations

• CSD.CV.modeOp k₀ a c d = if ∀ (k : Fin K), k ≠ k₀ → c k = d k then a (c k₀) (d k₀) else 0

theorem CSD.CV.modeOp_apply_of_agree {K N : ℕ} (k₀ : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) {c d : FieldConfig K N} (h : ∀ (k : Fin K), k ≠ k₀ → c k = d k) : modeOp k₀ a c d = a (c k₀) (d k₀)

theorem CSD.CV.modeOp_supportedOn {K N : ℕ} (k₀ : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) : SupportedOn {k₀} (modeOp k₀ a)

A single-mode operator is supported on that one mode. The support notion is not vacuous: every modeOp inhabits it.

theorem CSD.CV.commute_modeOp {K N : ℕ} {k₀ k₁ : Fin K} (h : k₀ ≠ k₁) (a b : Matrix (Fin N) (Fin N) ℂ) : modeOp k₀ a * modeOp k₁ b = modeOp k₁ b * modeOp k₀ a

Single-mode operators at distinct modes commute — for every pair of single-mode matrices. The concrete instance of commute_of_disjointSupport, and the reason the locality statement has content.