CV-5: free-field stroboscopic dynamics (the CV pillar meets the Floquet interface)

Category: 3-Local (CV track; CSD-free construction).

The free field's Hamiltonian is mode-diagonal (fieldHamiltonian = diagonal (fieldEnergy ·)), so its stroboscopic one-period evolution is an explicit diagonal-phase unitary — no matrix-exponential machinery is needed to build it, and the matrix exponential is recovered as a theorem:

• phaseDiagU f — the diagonal-phase unitary diag (e^{-i f(x)}) over ANY finite index (generic; the kicked-Ising phaseMat is the same shape).
• freeFieldU K N τ — one stroboscopic period of the free field: phases e^{-i τ E(c)} at the field energies E(c) = ∑ₖ oscEnergy (c k).
• ★ freeFieldU_eq_exp — legitimacy: the constructed step IS the matrix exponential exp (-(iτ) • H_field) (via Matrix.exp_diagonal), so "generated by the field Hamiltonian" is a theorem, not a reading.
• freeFieldFloquet K N τ — the field dynamics as a FloquetEvolution through the generic ofUnitaryMatrix seam: the whole §H interface API (exact information preservation at every period, induced projective dynamics, Loschmidt diagnostics) applies to the CV pillar verbatim.

The CSD-side closure (ontic lift on KSigma, record persistence) is instantiated in Empirical/CSD/QuantumChaos/FreeFieldClosure.lean; the locality consequence (mode-support preservation, dynamical commutation) is CV-6 (CV/DynamicalLocality.lean). Honest scope: finite cutoff throughout (K modes, N levels), free field only — interactions are outside this module's claims.

The diagonal-phase unitary, generically

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

Each diagonal phase entry annihilates its conjugate: conj (e^{-ir}) · e^{-ir} = 1.

noncomputable def CSD.CV.phaseDiagU {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : ι → ℝ) : ↥(Matrix.unitaryGroup ι ℂ)

The diagonal-phase unitary diag (e^{-i f(x)}) over any finite index: the one-period evolution of any diagonal Hamiltonian with (real) spectrum f.

Equations

• CSD.CV.phaseDiagU f = ⟨Matrix.diagonal fun (x : ι) => Complex.exp (-(Complex.I * ↑(f x))), ⋯⟩

@[simp]

theorem CSD.CV.phaseDiagU_val {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : ι → ℝ) : ↑(phaseDiagU f) = Matrix.diagonal fun (x : ι) => Complex.exp (-(Complex.I * ↑(f x)))

The free-field stroboscopic step

noncomputable def CSD.CV.freeFieldU (K N : ℕ) (τ : ℝ) : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)

One stroboscopic period of the free field: diagonal phases e^{-i τ E(c)} at the field energies.

Equations

• CSD.CV.freeFieldU K N τ = CSD.CV.phaseDiagU fun (c : CSD.CV.FieldConfig K N) => τ * CSD.CV.fieldEnergy c

theorem CSD.CV.phaseDiagU_eq_exp {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : ι → ℝ) : ↑(phaseDiagU f) = NormedSpace.exp (-Complex.I • Matrix.diagonal fun (x : ι) => ↑(f x))

Every diagonal-phase unitary is the matrix exponential of its (real diagonal) generator: phaseDiagU f = exp (−i • diag f). The generic exp-legitimacy seam — freeFieldU_eq_exp and the interacting drive's interactingU_eq_exp (CV/Interaction.lean) are instances.

theorem CSD.CV.freeFieldU_eq_exp (K N : ℕ) (τ : ℝ) : ↑(freeFieldU K N τ) = NormedSpace.exp (-(Complex.I * ↑τ) • fieldHamiltonian K N)

★ Legitimacy: the constructed step IS the matrix exponential of the field Hamiltonian, freeFieldU K N τ = exp (-(iτ) • H_field) — so "generated by H_field" is a theorem of the construction, not a gloss.

noncomputable def CSD.CV.freeFieldFloquet (K N : ℕ) (τ : ℝ) : QuantumChaos.FloquetEvolution (FieldSpace K N)

The free field as a Floquet evolution — the §H interface applies to the CV pillar verbatim: exact information preservation at every period, induced projective dynamics, Loschmidt diagnostics.

Equations

• CSD.CV.freeFieldFloquet K N τ = QuantumChaos.FloquetEvolution.ofUnitaryMatrix (CSD.CV.freeFieldU K N τ)