CV-10: finite-cutoff power counting — the price scales with operator grade

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

The honest finite content of EFT power counting: grade an interaction by its operator content (how many quadrature factors), and track how the CV-9 Duhamel price scales with the cutoff N:

• annihilation_l2_opNorm_le / Q_l2_opNorm_le — the norm-growth bricks: ‖a‖ ≤ √N (via the C*-identity ‖a‖² = ‖a†a‖ = ‖N̂‖ — no spectral asymptotics) and ‖Q‖ ≤ √(2N).
• l2_opNorm_modeOp_le — embedding a single-mode operator into the field does not increase its norm (modeOp is block-diagonal over the spectator configurations).
• gradedInteraction k m — the grade-m interaction Q_k^m on the field (Hermitian), with ‖Q_k^m‖ ≤ √(2N)^m.
• ★ gradedInteraction_price_le — the Duhamel price of the grade-m interaction is ≤ |τ|·|λ|·√(2N)^m: the certified price bound grows with the cutoff like N^{m/2}, exponent = the operator grade.
• ★★ gradedInteraction_renormalized_price_le — with the coupling renormalized as λ₀/√(2N)^m, the price is ≤ |τ|·|λ₀| — uniform in the cutoff. Cutoff-stability of a grade-m interaction's certified effect costs exactly the power N^{-m/2} of coupling: relevant / irrelevant as a theorem about the cutoff scaling of the price bound.

The contrast class needs no new theorem: a bounded potential (|v| ≤ C with C cutoff-independent — any density coupling with bounded g) is priced cutoff-uniformly at unrenormalized coupling by CV-9's interactingU_dist_le directly.

⚠️ Norms are the scoped Matrix.Norms.L2Operator (C) norm* throughout. Honest scope: these are upper bounds on the certified price, with no lower bounds — so no claim that an unrenormalized coupling actually diverges, and no claim the price is attained; "relevant/irrelevant" here means scaling of the bound, not an RG statement, and nothing continuum is asserted (ApproxCCR.no_exact_finite_ccr stands).

References

CV/Oscillator.lean (annihilation, creation, Q, creation_mul_annihilation); CV/ModeLocality.lean (modeOp); CV/InteractionPrice.lean (CV-9, freeField_perturbed_exp_dist_le); specs/cv-stage3-plan.md §3d; specs/future-work.md (row CV-10).

Norm growth of the single-mode operators

theorem CSD.CV.annihilation_l2_opNorm_le {N : ℕ} : ‖annihilation N‖ ≤ √↑N

The ladder-operator norm brick: ‖a‖ ≤ √N, by the C*-identity ‖a‖² = ‖a†a‖ = ‖N̂‖ and the diagonal bound — no spectral asymptotics.

theorem CSD.CV.creation_l2_opNorm_le {N : ℕ} : ‖creation N‖ ≤ √↑N

The creation operator has the same norm bound.

theorem CSD.CV.Q_l2_opNorm_le {N : ℕ} : ‖Q N‖ ≤ √(2 * ↑N)

The quadrature norm brick: ‖Q‖ ≤ √(2N).

Embedding into the field does not grow the norm

def CSD.CV.modeSplit {K N : ℕ} (k : Fin K) : FieldConfig K N ≃ ({ j : Fin K // j ≠ k } → Fin N) × Fin N

Split a configuration at mode k: the spectator assignment and the k-occupation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CSD.CV.modeSplit_symm_apply_self {K N : ℕ} (k : Fin K) (s : { j : Fin K // j ≠ k } → Fin N) (n : Fin N) : (modeSplit k).symm (s, n) k = n

theorem CSD.CV.update_modeSplit_symm {K N : ℕ} (k : Fin K) (s : { j : Fin K // j ≠ k } → Fin N) (n i : Fin N) : Function.update ((modeSplit k).symm (s, n)) k i = (modeSplit k).symm (s, i)

theorem CSD.CV.modeOp_mulVec_apply {K N : ℕ} (k : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) (x : FieldConfig K N → ℂ) (c : FieldConfig K N) : (modeOp k a).mulVec x c = ∑ n : Fin N, a (c k) n * x (Function.update c k n)

The field action of modeOp collapses to the single-mode action along the k-fibre.

theorem CSD.CV.l2_opNorm_modeOp_le {K N : ℕ} (k : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) : ‖modeOp k a‖ ≤ ‖a‖

Embedding a single-mode operator into the field does not increase its norm: modeOp is block-diagonal over the spectator configurations.

The graded interaction and its price

theorem CSD.CV.modeOp_conjTranspose {K N : ℕ} (k : Fin K) (a : Matrix (Fin N) (Fin N) ℂ) : (modeOp k a).conjTranspose = modeOp k a.conjTranspose

modeOp commutes with the adjoint.

noncomputable def CSD.CV.gradedInteraction (K : ℕ) {N : ℕ} (k : Fin K) (m : ℕ) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The grade-m interaction: Q_k^m — m quadrature factors on mode k, embedded in the field.

Equations

• CSD.CV.gradedInteraction K k m = CSD.CV.modeOp k (CSD.CV.Q N ^ m)

theorem CSD.CV.gradedInteraction_isHermitian {K N : ℕ} (k : Fin K) (m : ℕ) : (gradedInteraction K k m).IsHermitian

The graded interaction is Hermitian.

theorem CSD.CV.gradedInteraction_l2_opNorm_le {K N : ℕ} (k : Fin K) {m : ℕ} (hm : 0 < m) : ‖gradedInteraction K k m‖ ≤ √(2 * ↑N) ^ m

The graded interaction's norm grows at most like √(2N)^m — exponent = the operator grade.

theorem CSD.CV.gradedInteraction_price_le {K N : ℕ} [NeZero N] (τ lam : ℝ) (k : Fin K) {m : ℕ} (hm : 0 < m) : ‖NormedSpace.exp (-(Complex.I * ↑τ) • (fieldHamiltonian K N + lam • gradedInteraction K k m)) - ↑(freeFieldU K N τ)‖ ≤ |τ| * (|lam| * √(2 * ↑N) ^ m)

★ Power counting of the price: the Duhamel price of the grade-m interaction is ≤ |τ|·|λ|·√(2N)^m — the certified bound grows with the cutoff like N^{m/2}, exponent = the operator grade.

theorem CSD.CV.gradedInteraction_renormalized_price_le {K N : ℕ} [NeZero N] (τ lam₀ : ℝ) (k : Fin K) {m : ℕ} (hm : 0 < m) : ‖NormedSpace.exp (-(Complex.I * ↑τ) • (fieldHamiltonian K N + (lam₀ / √(2 * ↑N) ^ m) • gradedInteraction K k m)) - ↑(freeFieldU K N τ)‖ ≤ |τ| * |lam₀|

★★ Renormalization by the grade: with the coupling scaled as λ₀/√(2N)^m, the price of the grade-m interaction is ≤ |τ|·|λ₀| — uniform in the cutoff. Cutoff-stability of the certified effect costs exactly the power N^{-m/2} of coupling: relevant/irrelevant as a theorem about the cutoff scaling of the price bound.