CV-7: the interacting drive (EFT Stage 3a)

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

The first interacting object of the EFT chain. A diagonal (density–density) interaction commutes with the free Hamiltonian, so the interacting stroboscopic evolution is exact — one phaseDiagU, no Trotter step, no approximation to apologize for — and its generation by the interacting Hamiltonian is a theorem:

• densityCoupling k l g — the pair potential v c = g (c k) (c l): the interaction energy depends on the occupations of the two coupled modes (the kicked-Ising phaseMat is exactly this shape at K = N = 2).
• interactionHamiltonian v — diagonal v, Hermitian (interactionHamiltonian_isHermitian).
• interactingU K N τ lam v — one stroboscopic period of H_free + lam·V: diagonal phases e^{-iτ(E(c) + lam·v(c))}.
• ★ interactingU_eq_exp — legitimacy: interactingU = exp (-(iτ) • (H_field + lam • V)) (via the generic phaseDiagU_eq_exp) — "generated by the interacting Hamiltonian" is a theorem of the construction.
• interactingU_zero — switching the coupling off recovers the free field.
• interactingFloquet — the §H2 FloquetEvolution instance: the interface API (exact information preservation, projective dynamics, Loschmidt diagnostics) applies to the interacting drive verbatim.

The locality consequences — support spreading bounded by the coupling-graph light cone — are CV-8 (CV/SupportSpreading.lean); the CSD-side closure instance is in Empirical/CSD/QuantumChaos/FreeFieldClosure.lean. Honest scope: finite cutoff, diagonal interactions only — non-diagonal (hopping) interactions have no closed-form step and enter through the Duhamel pricing (CV-9), and nothing continuum is claimed.

References

CV/FreeFieldFloquet.lean (CV-5, phaseDiagU, phaseDiagU_eq_exp); CV/SupportSpreading.lean (CV-8); specs/cv-stage3-plan.md §3a; Incubator/QuantumChaos/KickedIsingPilot.lean (phaseMat, the prototype); specs/external-library-map.md §H; specs/future-work.md (row CV-7).

Diagonal interactions

def CSD.CV.densityCoupling {K N : ℕ} (k l : Fin K) (g : Fin N → Fin N → ℝ) : FieldConfig K N → ℝ

The density–density pair coupling: the interaction energy depends on the occupations of modes k and l through g.

Equations

• CSD.CV.densityCoupling k l g c = g (c k) (c l)

noncomputable def CSD.CV.interactionHamiltonian {K N : ℕ} (v : FieldConfig K N → ℝ) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The interaction Hamiltonian of a diagonal potential v: diagonal v in the configuration basis.

Equations

• CSD.CV.interactionHamiltonian v = Matrix.diagonal fun (c : CSD.CV.FieldConfig K N) => ↑(v c)

theorem CSD.CV.interactionHamiltonian_isHermitian {K N : ℕ} (v : FieldConfig K N → ℝ) : (interactionHamiltonian v).IsHermitian

A diagonal real potential is a Hermitian interaction.

The interacting stroboscopic step

noncomputable def CSD.CV.interactingU (K N : ℕ) (τ lam : ℝ) (v : FieldConfig K N → ℝ) : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

One stroboscopic period of the interacting field H_free + lam·V: diagonal phases e^{-iτ(E(c) + lam·v(c))}. Exact — a diagonal interaction commutes with the free Hamiltonian, so no Trotter splitting is involved.

Equations

• CSD.CV.interactingU K N τ lam v = CSD.CV.phaseDiagU fun (c : CSD.CV.FieldConfig K N) => τ * (CSD.CV.fieldEnergy c + lam * v c)

@[simp]

theorem CSD.CV.interactingU_val {K N : ℕ} (τ lam : ℝ) (v : FieldConfig K N → ℝ) : ↑(interactingU K N τ lam v) = Matrix.diagonal fun (c : FieldConfig K N) => Complex.exp (-(Complex.I * ↑(τ * (fieldEnergy c + lam * v c))))

theorem CSD.CV.interactingU_zero {K N : ℕ} (τ : ℝ) (v : FieldConfig K N → ℝ) : interactingU K N τ 0 v = freeFieldU K N τ

Switching the coupling off recovers the free field.

theorem CSD.CV.interactingU_eq_exp (K N : ℕ) (τ lam : ℝ) (v : FieldConfig K N → ℝ) : ↑(interactingU K N τ lam v) = NormedSpace.exp (-(Complex.I * ↑τ) • (fieldHamiltonian K N + lam • interactionHamiltonian v))

★ Legitimacy: the interacting step IS the matrix exponential of the interacting Hamiltonian, interactingU K N τ lam v = exp (-(iτ) • (H_field + lam • V)) — so "generated by H_free + lam·V" is a theorem of the construction, not a gloss.

noncomputable def CSD.CV.interactingFloquet (K N : ℕ) (τ lam : ℝ) (v : FieldConfig K N → ℝ) : QuantumChaos.FloquetEvolution (FieldSpace K N)

The interacting field as a Floquet evolution — the §H interface applies to the interacting drive verbatim.

Equations

• CSD.CV.interactingFloquet K N τ lam v = QuantumChaos.FloquetEvolution.ofUnitaryMatrix (CSD.CV.interactingU K N τ lam v)