CV-8 (i): the local algebra — SupportedOn is a unital *-subalgebra

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

CV/ModeLocality.lean defined SupportedOn S and proved that disjoint supports commute. This module upgrades the support notion to what Haag–Kastler actually posits: *the operators supported on S form a unital -subalgebra — the local algebra of the region, at the finite cutoff:

• SupportedOn.one, .add, .smul, .mul, .star — closure under the *-algebra operations. The product case is the load-bearing one: the surviving intermediate configurations of (A·B) c d agree with c off S, and the bijection e ↦ (e on S, c' off S) matches the two sums entry-for-entry.
• SupportedOn.mono — a bigger region supports everything the smaller one does. Not a formality: the indep field for the bigger region gives weaker hypotheses, and the proof needs the same offDiag-kills-both rescue as the product case (a mode moved in S' \ S zeroes both entries).

These are exactly the pieces the spreading bound needs (CV/SupportSpreading.lean): conjugation by a T-supported unitary lands in the S ∪ T algebra by star, mul, and mono alone.

References

CV/ModeLocality.lean (SupportedOn, commute_of_disjointSupport); CV/SupportSpreading.lean (CV-8 (ii)–(iv)); specs/cv-stage3-plan.md §3b; specs/future-work.md (row CV-8). Haag, Local Quantum Physics (1992).

Closure under the *-algebra operations

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

The identity is supported on every region.

theorem CSD.CV.SupportedOn.add {K N : ℕ} {S : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn S A) (hB : SupportedOn S B) : SupportedOn S (A + B)

Sums of S-supported operators are S-supported.

theorem CSD.CV.SupportedOn.sub {K N : ℕ} {S : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn S A) (hB : SupportedOn S B) : SupportedOn S (A - B)

Differences of S-supported operators are S-supported.

theorem CSD.CV.SupportedOn.smul {K N : ℕ} {S : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (z : ℂ) (hA : SupportedOn S A) : SupportedOn S (z • A)

Scalar multiples of S-supported operators are S-supported.

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

Adjoints of S-supported operators are S-supported.

theorem CSD.CV.SupportedOn.mul {K N : ℕ} {S : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn S A) (hB : SupportedOn S B) : SupportedOn S (A * B)

Products of S-supported operators are S-supported — the closure that makes SupportedOn S an algebra. The surviving intermediate configurations agree with c off S; the bijection e ↦ (e on S, c' off S) matches the two collapsed sums term-for-term.

Monotonicity

theorem CSD.CV.SupportedOn.mono {K N : ℕ} {S S' : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hSS' : S ⊆ S') (hA : SupportedOn S A) : SupportedOn S' A

Monotonicity: a bigger region supports everything the smaller one does. The indep case needs the offDiag rescue — a mode moved in S' \ S zeroes both entries.