CV-9: small-coupling pricing — locality violation is linear in the coupling

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

CV-8 bounded WHERE interaction moves support (the light cone); this module prices HOW MUCH, in operator norm, via the Duhamel bound (Matrix.norm_exp_smul_neg_I_sub_le, generalized to arbitrary finite index for exactly this use):

• freeField_perturbed_exp_dist_le — for ANY Hermitian perturbation V (diagonal or not — hopping interactions included): ‖exp (-(iτ)•(H_field + λ•V)) − freeFieldU τ‖ ≤ |τ|·|λ|·‖V‖. The pricing needs no closed-form step for the perturbed drive.
• ★ interactingU_dist_le — the CV-7 diagonal drive: with |v| ≤ C pointwise, ‖interactingU τ λ v − freeFieldU τ‖ ≤ |τ|·(|λ|·C) (the diagonal L2-norm bound Matrix.l2_opNorm_diagonal_le).
• heisenberg_dist_le — Heisenberg stability: conjugation by nearby unitaries moves any observable by at most 2·‖U − W‖·‖A‖ (C*-identity ‖U‖ = 1 + submultiplicativity).
• ★★ heisenberg_interactingU_near_supported — the price of locality violation: the interacting Heisenberg observable of an S-supported A stays within 2·|τ|·|λ|·C·‖A‖ of an S-supported operator (the free-evolved one, CV-6). Switching on a coupling λ costs locality at most linearly in λ — the CV rhyme of the record half-life bound μ ≤ n·ε (RecordDegradation.lean).

⚠️ All norms here are the scoped Matrix.Norms.L2Operator (C) norm* (open scoped Matrix.Norms.L2Operator), never the elementwise or Frobenius norm — consumers must open the same scope. Honest scope, both original boundaries since superseded: whether the linear price is attained was closed by CV/PriceAttainment.lean (P5-attainment, 2026-08-20 — a witness where the distance to the supported subalgebra is at least |sin(τλ/2)|, linear on both sides), and the non-diagonal light cone landed as CV-11 (eft-stage4-plan.md, exp-closure route, 2026-08-09).

References

CV/Interaction.lean (CV-7); CV/SupportSpreading.lean (CV-8); CV/DynamicalLocality.lean (CV-6, the free-evolved comparator); CsdLean4/Mathlib/Analysis/Matrix/DuhamelBound.lean (the engine); CsdLean4/Mathlib/Analysis/Matrix/L2OpNormDiagonal.lean; specs/cv-stage3-plan.md §3c; specs/future-work.md (row CV-9); Empirical/CSD/QuantumChaos/RecordDegradation.lean (the record-side rhyme).

instance CSD.CV.instNonemptyFieldConfig {K N : ℕ} [NeZero N] : Nonempty (FieldConfig K N)

Hermitian bookkeeping

theorem CSD.CV.isHermitian_diagonal_ofReal {ι : Type u_1} [DecidableEq ι] (w : ι → ℝ) : (Matrix.diagonal fun (i : ι) => ↑(w i)).IsHermitian

A real diagonal is Hermitian.

theorem CSD.CV.fieldHamiltonian_isHermitian (K N : ℕ) : (fieldHamiltonian K N).IsHermitian

The free-field Hamiltonian is Hermitian.

theorem CSD.CV.isHermitian_real_smul {K N : ℕ} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : A.IsHermitian) (r : ℝ) : (r • A).IsHermitian

Real scaling preserves Hermiticity.

The Duhamel price of a perturbation

theorem CSD.CV.neg_I_mul_smul_eq {K N : ℕ} {τ : ℝ} (M : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : -(Complex.I * ↑τ) • M = τ • -Complex.I • M

The -(iτ)-scaling in Schrödinger form, for the Duhamel interface.

theorem CSD.CV.freeField_perturbed_exp_dist_le {K N : ℕ} [NeZero N] (τ lam : ℝ) {V : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hV : V.IsHermitian) : ‖NormedSpace.exp (-(Complex.I * ↑τ) • (fieldHamiltonian K N + lam • V)) - ↑(freeFieldU K N τ)‖ ≤ |τ| * (|lam| * ‖V‖)

The Duhamel price of any Hermitian perturbation — diagonal or not, no closed-form step needed: ‖exp (-(iτ)•(H_field + λ•V)) − freeFieldU τ‖ ≤ |τ|·(|λ|·‖V‖).

theorem CSD.CV.interactingU_dist_le {K N : ℕ} [NeZero N] (τ lam : ℝ) (v : FieldConfig K N → ℝ) {C : ℝ} (hC : 0 ≤ C) (hv : ∀ (c : FieldConfig K N), |v c| ≤ C) : ‖↑(interactingU K N τ lam v) - ↑(freeFieldU K N τ)‖ ≤ |τ| * (|lam| * C)

★ The interacting drive stays within |τ|·|λ|·C of the free drive when the potential is pointwise bounded by C — the CV-7 step, priced.

Heisenberg stability and the price of locality violation

theorem CSD.CV.heisenberg_dist_le {K N : ℕ} [NeZero N] (U W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : ‖heisenberg U A - heisenberg W A‖ ≤ 2 * ‖↑U - ↑W‖ * ‖A‖

Heisenberg stability: conjugation by nearby unitaries moves any observable by at most 2·‖U − W‖·‖A‖ (C*-identity + submultiplicativity).

theorem CSD.CV.heisenberg_interactingU_dist_le {K N : ℕ} [NeZero N] (τ lam : ℝ) (v : FieldConfig K N → ℝ) {C : ℝ} (hC : 0 ≤ C) (hv : ∀ (c : FieldConfig K N), |v c| ≤ C) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : ‖heisenberg (interactingU K N τ lam v) A - heisenberg (freeFieldU K N τ) A‖ ≤ 2 * (|τ| * (|lam| * C)) * ‖A‖

The interacting Heisenberg observable stays within 2·|τ|·|λ|·C·‖A‖ of the free-evolved one.

theorem CSD.CV.heisenberg_interactingU_near_supported {K N : ℕ} [NeZero N] {S : Finset (Fin K)} (τ lam : ℝ) (v : FieldConfig K N → ℝ) {C : ℝ} (hC : 0 ≤ C) (hv : ∀ (c : FieldConfig K N), |v c| ≤ C) {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn S A) : ∃ (B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ), SupportedOn S B ∧ ‖heisenberg (interactingU K N τ lam v) A - B‖ ≤ 2 * (|τ| * (|lam| * C)) * ‖A‖

★★ The price of locality violation is linear in the coupling: the interacting Heisenberg observable of an S-supported A stays within 2·|τ|·|λ|·C·‖A‖ of an S-supported operator — the free-evolved one, which CV-6 keeps on S exactly. The CV rhyme of the record half-life bound μ ≤ n·ε.