The quantum-chaos pilot capstone (H3)

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

The §H3 pilot statement, as one citable closure: a repeated finite-dimensional unitary evolution preserves global information, may change restricted accessibility, induces projective dynamics, admits an ontic lift under stated hypotheses, and preserves a formed record when the record sector is invariant.

FloquetPilotClosure U p₀ bundles the four universal clauses for any unitary-generated step (fields quantified over all period counts n), and floquetPilotClosure discharges it for EVERY unitary U and base point p₀ — existence by construction, on the corpus's own sector machinery. The existential clause ("MAY change restricted accessibility") is witnessed separately by the concrete model: ★ kickedIsing_changes_marginal (Incubator/QuantumChaos/KickedIsingPilot.lean) — at kick angle π/2 the two-qubit kicked-Ising step moves the reduced first-qubit state while every global overlap is exactly invariant.

Like the corpus's other capstones, this is a witness/feature index over the named constituents (a consistency closure), not a uniqueness or emergence claim; the constituent theorems are the citable content. Scope: the ontic lift is the canonical fibre-fixing one on KSigma N for Fin N-indexed steps; record persistence is under the product-form (uncoupled) hypothesis — coupled post-record driving is the thread's open continuation. See specs/external-library-map.md §H and specs/future-work.md.

structure CSD.Empirical.QuantumChaos.FloquetPilotClosure {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) : Prop

The pilot closure: the four universal clauses of the §H3 statement for a unitary-generated Floquet evolution, at every period count.

• info_preserved (n : ℕ) (u v : EuclideanSpace ℂ (Fin N)) : inner ℂ (((QuantumChaos.FloquetEvolution.ofUnitary U).iterate n) u) (((QuantumChaos.FloquetEvolution.ofUnitary U).iterate n) v) = inner ℂ u v

  Global information is preserved: every overlap is an exact invariant of every period count.

• projective (n : ℕ) : Projectivization.TransProbPreserving ((QuantumChaos.FloquetEvolution.ofUnitary U).projIterate n)

  Projective dynamics is induced, transition-probability preserving at every period count (the wigner_rigidity hypothesis).

• ontic_measure (n : ℕ) : MeasureTheory.MeasurePreserving (floquetOnticStep U)^[n] (LF4.kMuL p₀) (LF4.kMuL p₀)

  The ontic lift preserves the Liouville measure at every period count.

• ontic_projects (n : ℕ) (x : LF4.KSigma N) : ((floquetOnticStep U)^[n] x).1 = (QuantumChaos.FloquetEvolution.ofUnitary U).projIterate n x.1

  The ontic lift projects to the ray dynamics, period by period.

• records_persist (Rec : Type) (S : Set Rec) (n : ℕ) : (floquetRecordStep U Rec)^[n] ⁻¹' Prod.snd ⁻¹' S = Prod.snd ⁻¹' S

  Formed records persist surely under uncoupled post-record driving: every record cylinder is set-invariant at every period count.

theorem CSD.Empirical.QuantumChaos.floquetPilotClosure {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) : FloquetPilotClosure U p₀

★★ The pilot closure holds for every unitary-generated Floquet evolution — the §H3 vertical result, discharged on the corpus's own sector machinery. The accessibility-change clause is witnessed by the concrete model: kickedIsing_changes_marginal.

theorem CSD.Empirical.QuantumChaos.kickedIsing_pilotClosure (J b : ℝ) (p₀ : LF4.CPN 4) : FloquetPilotClosure (QuantumChaos.kickedIsingU₄ J b) p₀

★ The concrete model reaches the ontic-lift clause: the kicked-Ising pilot closure at Fin 4 (through the finProdFinEquiv reindex kickedIsingU₄), for every parameter pair and base point.