The free field reaches the pilot closure (CV-5, CSD side)

Category: 6-Empirical-CSD (the CSD reading of stroboscopic dynamics).

CV/FreeFieldFloquet.lean built the free field's stroboscopic step (freeFieldU, a diagonal-phase unitary provably equal to exp (-(iτ) • H_field)). This module carries it into the §H3 ontic machinery, which is stated over Fin-indexed unitaries:

• card_fieldConfig — the configuration space has N ^ K points.

• freeFieldUFin — the free-field step reindexed to Fin (card (FieldConfig K N)) along Fintype.equivFin (unitarity by reindex_mem_unitaryGroup, the same seam the kicked-Ising pilot used for kickedIsingU₄).

• ★ freeField_pilotClosure — the CV pillar satisfies the full §H3 pilot closure: exact information preservation at every period, induced projective dynamics, the measure-preserving ontic lift on KSigma, and sure record persistence under uncoupled post-record driving — for every cutoff (K, N), period τ, and base point.

• ★ interacting_pilotClosure (CV-7 CSD side) — the closure also covers every diagonal interaction at every coupling strength (interactingUFin): the closure clauses are about unitarity, not freeness.

So the quantum-chaos vertical (interface → ontic lift → records) and the CV vertical (modes → free field → interactions) meet: the same closure instance covers the kicked-Ising model, the free field, and the interacting field at a cutoff. Honest scope: diagonal (density-coupled) drives at a finite cutoff; coupled record driving is priced separately (RecordDegradation.lean, CouplingWitness.lean), and non-diagonal (hopping) interactions enter through the CV-9 pricing route.

References

CV/FreeFieldFloquet.lean (CV-5, the step and its exp-legitimacy); CV/DynamicalLocality.lean (CV-6, the locality consequence); Empirical/CSD/QuantumChaos/Capstone.lean (FloquetPilotClosure); Incubator/QuantumChaos/KickedIsingPilot.lean (reindex_mem_unitaryGroup); specs/external-library-map.md §H; specs/BACKLOG.md; specs/future-work.md.

theorem CSD.Empirical.QuantumChaos.card_fieldConfig (K N : ℕ) : Fintype.card (CV.FieldConfig K N) = N ^ K

The configuration space of K modes at N levels has N ^ K points.

instance CSD.Empirical.QuantumChaos.instNeZeroNatCardFieldConfig {K N : ℕ} [NeZero N] : NeZero (Fintype.card (CV.FieldConfig K N))

noncomputable def CSD.Empirical.QuantumChaos.freeFieldUFin (K N : ℕ) (τ : ℝ) : ↥(Matrix.unitaryGroup (Fin (Fintype.card (CV.FieldConfig K N))) ℂ)

The free-field stroboscopic step, reindexed to Fin (card (FieldConfig K N)) so the Fin N ontic machinery (KSigma, floquetOnticStep, the pilot closure) applies directly.

Equations

• CSD.Empirical.QuantumChaos.freeFieldUFin K N τ = ⟨(Matrix.reindex (Fintype.equivFin (CSD.CV.FieldConfig K N)) (Fintype.equivFin (CSD.CV.FieldConfig K N))) ↑(CSD.CV.freeFieldU K N τ), ⋯⟩

theorem CSD.Empirical.QuantumChaos.freeField_pilotClosure {K N : ℕ} [NeZero N] (τ : ℝ) (p₀ : LF4.CPN (Fintype.card (CV.FieldConfig K N))) : FloquetPilotClosure (freeFieldUFin K N τ) p₀

★ The CV pillar reaches the §H3 pilot closure: the free field at any cutoff satisfies all four universal clauses — information preservation, induced projective dynamics, the measure-preserving ontic lift, and sure record persistence — for every period τ and base point.

noncomputable def CSD.Empirical.QuantumChaos.interactingUFin (K N : ℕ) (τ lam : ℝ) (v : CV.FieldConfig K N → ℝ) : ↥(Matrix.unitaryGroup (Fin (Fintype.card (CV.FieldConfig K N))) ℂ)

The interacting drive (CV-7), reindexed to Fin (card (FieldConfig K N)) along the same seam.

Equations

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

theorem CSD.Empirical.QuantumChaos.interacting_pilotClosure {K N : ℕ} [NeZero N] (τ lam : ℝ) (v : CV.FieldConfig K N → ℝ) (p₀ : LF4.CPN (Fintype.card (CV.FieldConfig K N))) : FloquetPilotClosure (interactingUFin K N τ lam v) p₀

★ The interacting drive reaches the §H3 pilot closure too — every diagonal interaction, at every coupling strength: the closure clauses are about unitarity, not freeness.