CV-26: channel-level RG at the cutoff — coarse-graining with a priced defect

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

The Stage-4 no-go (exists_unitary_compress_not_unitary) proved that exact unitary RG matching is impossible: decimating a support-spreading drive loses norm. Its own conclusion was that an honest RG statement has to be about channels with an error budget. This module is that statement.

The coarse-graining is mode tracing: keep the spectator modes, discard mode k.

• coarseIsom k / coarseChannel k — the coarse-graining as a genuine CPTP map, built as the Stinespring channel of the mode-split permutation isometry (Channel.ofIsometry), so complete positivity and trace preservation come for free. coarseChannel_apply_entry: C(ρ)ᵢⱼ = ∑ₘ ρ(i⊕m, j⊕m) — trace out mode k.

• spectatorEnergy / spectatorU — the coarse system's own free drive, the diagonal phase of the spectator energy. fieldEnergy_modeSplit_symm is the split that makes it work: E(s ⊕ m) = E_spec(s) + E_osc(m).

• ★ coarseChannel_free_intertwine (CR-2) — the free drive intertwines the coarse-graining exactly: C(F ρ F†) = U_eff · C(ρ) · U_eff†. The traced mode's phase cancels against its own conjugate under the trace — the same m appears on both sides of every surviving entry — so no error is incurred: at zero coupling the RG step is exact, and the whole budget below is the price of the interaction.

• ★★ channelRG_dist_le (CR-3, the capstone) — the priced RG step:

  D( C(U^n ρ U^{n†}), U_eff^n · C(ρ) · U_eff^{n†} ) ≤ 2n·|τ|·|λ|·C

  for every density operator ρ. Coarse-graining the interacting evolution and evolving the coarse-grained state with the free effective drive agree up to a defect linear in the period count and in the coupling — the channel-level replacement for the matching the no-go forbids.

The budget, and where each factor comes from

2 from the unitary-perturbation bridge (traceDist_conj_sub_le, CR-1); n from the growth-free telescoping (Matrix.norm_pow_sub_pow_le_of_unitary, CV-12); |τ|·|λ|·C from the one-period Duhamel price (interactingU_dist_le, CV-9). The data-processing inequality (channel_traceDist_le, K3) is what lets the coarse-graining be applied after the estimate rather than before — it is the step that makes a channel-level statement cheaper than an operator-level one, not more expensive.

⚠️ Honest scope, unchanged from the scoping pass. No RG flow: this is one coarse-graining step with a priced defect — no iteration, no fixed point, no beta function. No level decimation: the compressCfg route of CV-16 is trace-decreasing and needs a leakage arm the corpus does not have; mode tracing is the route that is CPTP today. Uniform in distance: the cone-refined budget ε(distance) is a deferred refinement, not claimed here. No continuum limit (ApproxCCR.no_exact_finite_ccr stands); the diamond norm is not used, and no claim is made beyond per-state trace distance.

References

specs/channel-rg-scoping.md (the CV-25 scoping pass: rows CR-1/CR-2/CR-3, the budget chain, the wall-checks this module discharges); specs/BACKLOG.md (Q21 → CV-26); specs/future-work.md (row CV-26); CV/Decimation.lean (CV-16, the no-go this answers); Mathlib/QuantumInfo/UnitaryPerturbation.lean (CR-1, traceDist_conj_sub_le); Mathlib/QuantumInfo/DataProcessing.lean (channel_traceDist_le); Mathlib/QuantumInfo/Stinespring.lean (Channel.ofIsometry); CV/PowerCounting.lean (modeSplit); CV/InteractionPrice.lean (interactingU_dist_le); CV/FreeFieldFloquet.lean (phaseDiagU, freeFieldU).

The coarse system: spectator modes

@[reducible, inline]

abbrev CSD.CV.SpectatorCfg (K N : ℕ) (k : Fin K) : Type

The spectator configuration space: the occupation configuration of every mode but k — the system that survives the coarse-graining.

Equations

• CSD.CV.SpectatorCfg K N k = ({ j : Fin K // j ≠ k } → Fin N)

noncomputable def CSD.CV.spectatorEnergy {K N : ℕ} (k : Fin K) (s : SpectatorCfg K N k) : ℝ

The spectator energy: the free energy carried by the modes the coarse-graining keeps.

Equations

• CSD.CV.spectatorEnergy k s = ∑ j : { j : Fin K // j ≠ k }, CSD.CV.oscEnergy ↑(s j)

theorem CSD.CV.fieldEnergy_modeSplit_symm {K N : ℕ} (k : Fin K) (s : SpectatorCfg K N k) (m : Fin N) : fieldEnergy ((modeSplit k).symm (s, m)) = spectatorEnergy k s + oscEnergy ↑m

The energy splits across the mode split: E(s ⊕ m) = E_spec(s) + E_osc(m). This additivity is what makes the free drive factorise, and hence CR-2 exact.

The coarse-graining channel

noncomputable def CSD.CV.coarseIsom {K N : ℕ} (k : Fin K) : Matrix (SpectatorCfg K N k × Fin N) (FieldConfig K N) ℂ

The mode-split isometry: the permutation matrix carrying a field configuration to its (spectators, mode-k) pair.

Equations

• CSD.CV.coarseIsom k = Matrix.of fun (p : CSD.CV.SpectatorCfg K N k × Fin N) (c : CSD.CV.FieldConfig K N) => if p = (CSD.CV.modeSplit k) c then 1 else 0

@[simp]

theorem CSD.CV.coarseIsom_apply {K N : ℕ} (k : Fin K) (p : SpectatorCfg K N k × Fin N) (c : FieldConfig K N) : coarseIsom k p c = if p = (modeSplit k) c then 1 else 0

theorem CSD.CV.coarseIsom_isometry {K N : ℕ} (k : Fin K) : (coarseIsom k).conjTranspose * coarseIsom k = 1

The mode-split matrix is an isometry — it is a permutation of the index set.

noncomputable def CSD.CV.coarseChannel {K N : ℕ} (k : Fin K) : QuantumInfo.Channel (FieldConfig K N) (SpectatorCfg K N k) (Fin N)

★ The coarse-graining channel: trace out mode k, keeping the spectators. A genuine CPTP map — the Stinespring channel of the mode-split isometry — so the data-processing inequality applies to it.

Equations

• CSD.CV.coarseChannel k = QuantumInfo.Channel.ofIsometry (CSD.CV.coarseIsom k) ⋯

theorem CSD.CV.coarseIsom_conj {K N : ℕ} (k : Fin K) (X : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (p q : SpectatorCfg K N k × Fin N) : (coarseIsom k * X * (coarseIsom k).conjTranspose) p q = X ((modeSplit k).symm p) ((modeSplit k).symm q)

Conjugating by the mode-split isometry is reindexing.

theorem CSD.CV.coarseChannel_apply_entry {K N : ℕ} (k : Fin K) (ρ : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (i j : SpectatorCfg K N k) : (coarseChannel k).apply ρ i j = ∑ m : Fin N, ρ ((modeSplit k).symm (i, m)) ((modeSplit k).symm (j, m))

The coarse-graining, entrywise: C(ρ)ᵢⱼ = ∑ₘ ρ(i ⊕ m, j ⊕ m) — mode k is traced out.

The effective (coarse) free drive

noncomputable def CSD.CV.spectatorU {K N : ℕ} (k : Fin K) (θ : ℝ) : ↥(Matrix.unitaryGroup (SpectatorCfg K N k) ℂ)

The effective free drive on the coarse system: the diagonal phase of the spectator energy.

Equations

• CSD.CV.spectatorU k θ = CSD.CV.phaseDiagU fun (s : CSD.CV.SpectatorCfg K N k) => θ * CSD.CV.spectatorEnergy k s

theorem CSD.CV.spectatorU_pow {K N : ℕ} (k : Fin K) (τ : ℝ) (n : ℕ) : spectatorU k τ ^ n = spectatorU k (↑n * τ)

The effective drive at n periods is the n-th power of the one-period drive — the coarse dynamics is a genuine stroboscopic evolution.

theorem CSD.CV.exp_phase_mul_star_self (r : ℝ) : Complex.exp (-(Complex.I * ↑r)) * star (Complex.exp (-(Complex.I * ↑r))) = 1

A pure phase times its own conjugate is 1 — the cancellation that makes the traced mode drop out of CR-2.

theorem CSD.CV.diagonal_conj_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : ι → ℂ) (X : Matrix ι ι ℂ) (i j : ι) : (Matrix.diagonal g * X * (Matrix.diagonal g).conjTranspose) i j = g i * X i j * star (g j)

Conjugation by a diagonal matrix, entrywise.

theorem CSD.CV.coarseChannel_free_intertwine {K N : ℕ} (k : Fin K) (τ : ℝ) (n : ℕ) (ρ : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : (coarseChannel k).apply (↑(freeFieldU K N τ ^ n) * ρ * (↑(freeFieldU K N τ ^ n)).conjTranspose) = ↑(spectatorU k (↑n * τ)) * (coarseChannel k).apply ρ * (↑(spectatorU k (↑n * τ))).conjTranspose

★ CR-2: the free drive intertwines the coarse-graining exactly. C(F ρ F†) = U_eff · C(ρ) · U_eff†, with no error term: the traced mode's phase meets its own conjugate in every surviving entry and cancels. At zero coupling the RG step is exact — every bit of the CR-3 budget is the price of the interaction.

The priced RG step

theorem CSD.CV.isHermitian_unitary_conj {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A ρ : Matrix ι ι ℂ} (hρ : ρ.IsHermitian) : (A * ρ * A.conjTranspose).IsHermitian

Conjugation by a unitary preserves Hermiticity.

theorem CSD.CV.trace_unitary_conj {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A ρ : Matrix ι ι ℂ} (hA : A.conjTranspose * A = 1) : (A * ρ * A.conjTranspose).trace = ρ.trace

Conjugation by a unitary preserves the trace.

noncomputable def CSD.CV.coarseInteracting {K N : ℕ} (k : Fin K) (τ lam : ℝ) (v : FieldConfig K N → ℝ) (n : ℕ) (ρ : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : Matrix (SpectatorCfg K N k) (SpectatorCfg K N k) ℂ

The coarse-grained interacting evolution: run the true (interacting) dynamics for n periods, then coarse-grain.

Equations

• CSD.CV.coarseInteracting k τ lam v n ρ = (CSD.CV.coarseChannel k).apply (↑(CSD.CV.interactingU K N τ lam v ^ n) * ρ * (↑(CSD.CV.interactingU K N τ lam v ^ n)).conjTranspose)

noncomputable def CSD.CV.coarseEffective {K N : ℕ} (k : Fin K) (τ : ℝ) (n : ℕ) (ρ : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : Matrix (SpectatorCfg K N k) (SpectatorCfg K N k) ℂ

The effective coarse evolution: coarse-grain first, then run the free effective drive on the coarse system for n periods.

Equations

• CSD.CV.coarseEffective k τ n ρ = ↑(CSD.CV.spectatorU k (↑n * τ)) * (CSD.CV.coarseChannel k).apply ρ * (↑(CSD.CV.spectatorU k (↑n * τ))).conjTranspose

theorem CSD.CV.coarseInteracting_def {K N : ℕ} (k : Fin K) (τ lam : ℝ) (v : FieldConfig K N → ℝ) (n : ℕ) (ρ : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : coarseInteracting k τ lam v n ρ = (coarseChannel k).apply (↑(interactingU K N τ lam v ^ n) * ρ * (↑(interactingU K N τ lam v ^ n)).conjTranspose)

theorem CSD.CV.coarseEffective_def {K N : ℕ} (k : Fin K) (τ : ℝ) (n : ℕ) (ρ : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : coarseEffective k τ n ρ = ↑(spectatorU k (↑n * τ)) * (coarseChannel k).apply ρ * (↑(spectatorU k (↑n * τ))).conjTranspose

theorem CSD.CV.coarseEffective_eq_coarse_free {K N : ℕ} (k : Fin K) (τ : ℝ) (n : ℕ) (ρ : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : coarseEffective k τ n ρ = (coarseChannel k).apply (↑(freeFieldU K N τ ^ n) * ρ * (↑(freeFieldU K N τ ^ n)).conjTranspose)

The RG step is exact at zero coupling: the effective coarse evolution IS the coarse-grained free evolution (CR-2, in the named form the capstone consumes).

theorem CSD.CV.channelRG_dist_le {K N : ℕ} [NeZero N] (k : Fin K) (τ lam : ℝ) (v : FieldConfig K N → ℝ) {C : ℝ} (hC : 0 ≤ C) (hv : ∀ (c : FieldConfig K N), |v c| ≤ C) (n : ℕ) {ρ : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hρ : ρ.PosSemidef) (htr : ρ.trace = 1) (h : (coarseInteracting k τ lam v n ρ - coarseEffective k τ n ρ).IsHermitian) : QuantumInfo.traceDist h ≤ 2 * (↑n * (|τ| * (|lam| * C)))

★★ CR-3: the channel-level RG step, priced (the CV-26 capstone).

D( C(U^n ρ U^{n†}), U_eff^n · C(ρ) · U_eff^{n†} ) ≤ 2n·|τ|·|λ|·C

for every density operator ρ: coarse-graining the interacting evolution and running the coarse-grained state under the free effective drive agree up to a defect linear in the period count and in the coupling strength.

This is the statement the Stage-4 no-go said had to replace unitary RG matching (exists_unitary_compress_not_unitary: exact unitary matching is impossible for support-spreading drives). The coarse-graining is CPTP, the comparison is in trace distance, and the defect is the CV-9 Duhamel price carried through the CV-12 telescoping by the CR-1 bridge, with the data-processing inequality applying the channel after the estimate.

⚠️ One coarse-graining step, not a flow: no iteration, no fixed point, no beta function. The bound is uniform in ρ and in the distance between modes.