The ontic lift of a Floquet evolution (quantum-chaos workstream, H3)

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

The "admits an ontic lift under stated hypotheses" clause of the §H3 pilot: every unitary-generated Floquet step (FloquetEvolution.ofUnitary U — one of the exactly two classes wigner_rigidity allows) lifts to a Liouville- preserving step on the ontic sector Σ = ℂℙ^{N-1} × T² (LF4.KSigma), whose projection is the interface's ray dynamics.

• floquetOnticStep U — the Σ-level step (p, θ) ↦ (U • p, θ): the ray is rotated, the fibre rides along. Definitionally the time-1 flow of the constant-family manyToOneSetup, so measure preservation is inherited, not re-proved (floquetOnticStep_measurePreserving).
• ofUnitary_projStep_smul — the interface's ray step for ofUnitary U IS the U • · action on ℂℙ^{N-1}.
• ★ floquetOnticStep_lifts / floquetOnticStep_iterate_lifts — the lift equations: π ∘ Φ = projStep ∘ π, and for every n, π ∘ Φ^[n] = projIterate n ∘ π — the ontic step projects to the interface's ray dynamics, period by period.

Stated hypotheses, honestly: the step is unitary-generated (ofUnitary U on Fin N; the kicked-Ising model's product index reaches this via reindexing, an §H follow-up), and the lift presented is the canonical fibre-fixing one — existence, not uniqueness. Cross-references: specs/external-library-map.md (the workstream architecture), specs/future-work.md (long-horizon rows), LF4/ManyToOnePillars.lean (the reused sector machinery).

noncomputable def CSD.Empirical.QuantumChaos.floquetOnticStep {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : LF4.KSigma N → LF4.KSigma N

The ontic (Σ-level) one-period step of a unitary-generated Floquet evolution: rotate the ray, fix the fibre. Definitionally the time-1 flow of the constant-family manyToOneSetup.

Equations

• CSD.Empirical.QuantumChaos.floquetOnticStep U x = (U • x.1, x.2)

theorem CSD.Empirical.QuantumChaos.floquetOnticStep_measurePreserving {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) : MeasureTheory.MeasurePreserving (floquetOnticStep U) (LF4.kMuL p₀) (LF4.kMuL p₀)

The ontic step preserves the Liouville measure kMuL = μ_FS ⊗ vol — inherited from the constant-family manyToOneSetup's flow, not re-proved.

theorem CSD.Empirical.QuantumChaos.floquetOnticStep_iterate_measurePreserving {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) (n : ℕ) : MeasureTheory.MeasurePreserving (floquetOnticStep U)^[n] (LF4.kMuL p₀) (LF4.kMuL p₀)

Iterates of the ontic step preserve the Liouville measure.

theorem CSD.Empirical.QuantumChaos.ofUnitary_projStep_smul {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : (QuantumChaos.FloquetEvolution.ofUnitary U).projStep p = U • p

The interface's ray step for ofUnitary U is the U • · action on ℂℙ^{N-1} (bridging projMap of the adapter's isometry to the corpus's MulAction).

theorem CSD.Empirical.QuantumChaos.floquetOnticStep_lifts {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (x : LF4.KSigma N) : (floquetOnticStep U x).1 = (QuantumChaos.FloquetEvolution.ofUnitary U).projStep x.1

★ The lift equation: the ontic step projects to the interface's ray dynamics — π (Φ x) = projStep (π x) with π = Prod.fst.

theorem CSD.Empirical.QuantumChaos.ofUnitary_projIterate_smul {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (n : ℕ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : (QuantumChaos.FloquetEvolution.ofUnitary U).projIterate n p = (fun (x : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => U • x)^[n] p

The iterated ray dynamics is iterated smul.

theorem CSD.Empirical.QuantumChaos.floquetOnticStep_iterate_lifts {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (n : ℕ) (x : LF4.KSigma N) : ((floquetOnticStep U)^[n] x).1 = (QuantumChaos.FloquetEvolution.ofUnitary U).projIterate n x.1

★ The iterated lift equation: for every period count n, π (Φ^[n] x) = projIterate n (π x) — the ontic dynamics projects to the interface's ray dynamics, period by period.