The Floquet-evolution interface (quantum-chaos workstream, H2)

Category: Special (incubator — CSD-free; upstream-candidate(physlib)).

The small abstract interface the CSD quantum-chaos theorems bind to (BACKLOG §H2; policy in specs/external-library-map.md): one stroboscopic period of a periodically driven finite quantum system, as a linear isometry equivalence — an equivalence, not merely an isometry, because reversibility is load-bearing for the CSD reading (global information preservation, records).

Four-way classification (checked 2026-08-07 against the actual repositories): Mathlib has the matrix exponential and unitary machinery but no Floquet notion; Physlib (leanprover-community/physlib, Lean 4.32.0, 690 modules) has a genuine QuantumMechanics/HilbertSpaces/FiniteTarget layer — a structure wrapping EuclideanSpace ℂ d, so future adapters are .val-thin — but no Floquet, kicked-model, or chaos-diagnostic modules. Hence class 3: implemented locally behind this interface, marked upstream-candidate(physlib); when Physlib grows the generic notion (or this file moves there), adapters in CsdLean4/Interop/ replace it and the CSD theorems downstream are untouched.

API

• FloquetEvolution H — the interface: step : H ≃ₗᵢ[ℂ] H.
• iterate n = step ^ n — n stroboscopic periods (the group structure on H ≃ₗᵢ[ℂ] H supplies the power), with iterate_zero/one/succ_apply and the ★ information-preservation lemmas norm_iterate_apply / inner_iterate_iterate (global norms and overlaps are exact invariants of arbitrarily many periods — the "preserves global information" clause of the §H3 pilot statement).
• projStep / projIterate — the induced ray dynamics on ℙ ℂ H (Projectivization.projMap), with functoriality (projIterate_succ, via projMap_trans) and, on ℂℙ^{N-1}, transition- probability preservation (projStep_transProbPreserving, projIterate_transProbPreserving) — the "induces projective dynamics" clause, in exactly the vocabulary wigner_rigidity consumes.
• refl and ofUnitary — inhabitation and the matrix-dynamics adapter seam: one period generated by a unitary matrix on ℂ^N (kicked models are products of such steps), through the staged toEuclideanLinearEquiv + inner_toEuclideanLin_unitary.

The CSD-side content (ontic lift, Σ-volume preservation, record persistence) deliberately does NOT live here: it binds to this interface from Empirical/CSD/QuantumChaos/ (§H3).

structure QuantumChaos.FloquetEvolution (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Type u_1

The Floquet-evolution interface: one stroboscopic period of a periodically driven system on the state space H, as a linear isometry equivalence. CSD theorems bind to this structure; adapters instantiate it (local matrix dynamics now, Physlib finite-system dynamics later).

• step : H ≃ₗᵢ[ℂ] H

  One period of the drive. An equivalence: the evolution is reversible.

noncomputable def QuantumChaos.FloquetEvolution.iterate {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) (n : ℕ) : H ≃ₗᵢ[ℂ] H

n stroboscopic periods: the n-th power of the step in the group of linear isometry equivalences.

Equations

• F.iterate n = F.step ^ n

@[simp]

theorem QuantumChaos.FloquetEvolution.iterate_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) : F.iterate 0 = 1

@[simp]

theorem QuantumChaos.FloquetEvolution.iterate_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) : F.iterate 1 = F.step

theorem QuantumChaos.FloquetEvolution.iterate_succ_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) (n : ℕ) (ψ : H) : (F.iterate (n + 1)) ψ = (F.iterate n) (F.step ψ)

Peeling one period at the start: iterate (n+1) ψ = iterate n (step ψ).

theorem QuantumChaos.FloquetEvolution.iterate_succ_apply' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) (n : ℕ) (ψ : H) : (F.iterate (n + 1)) ψ = F.step ((F.iterate n) ψ)

Peeling one period at the end: iterate (n+1) ψ = step (iterate n ψ).

@[simp]

theorem QuantumChaos.FloquetEvolution.norm_iterate_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) (n : ℕ) (ψ : H) : ‖(F.iterate n) ψ‖ = ‖ψ‖

★ Global information preservation (norms). The norm is an exact invariant of arbitrarily many periods.

@[simp]

theorem QuantumChaos.FloquetEvolution.inner_iterate_iterate {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) (n : ℕ) (u v : H) : inner ℂ ((F.iterate n) u) ((F.iterate n) v) = inner ℂ u v

★ Global information preservation (overlaps). Inner products are exact invariants of arbitrarily many periods: no global information is lost, however scrambled the local accessibility becomes.

The induced projective (ray) dynamics

noncomputable def QuantumChaos.FloquetEvolution.projStep {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) : Projectivization ℂ H → Projectivization ℂ H

The ray dynamics of one period on ℙ ℂ H.

Equations

• F.projStep = Projectivization.projMap F.step

noncomputable def QuantumChaos.FloquetEvolution.projIterate {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) (n : ℕ) : Projectivization ℂ H → Projectivization ℂ H

The ray dynamics of n periods.

Equations

• F.projIterate n = Projectivization.projMap (F.iterate n)

@[simp]

theorem QuantumChaos.FloquetEvolution.projIterate_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) : F.projIterate 0 = id

theorem QuantumChaos.FloquetEvolution.projIterate_succ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) (n : ℕ) : F.projIterate (n + 1) = F.projStep ∘ F.projIterate n

The ray dynamics iterates with the vector dynamics: n+1 periods on rays is one ray period after n (functoriality of projMap).

Transition-probability preservation on ℂℙ^{N-1}

theorem QuantumChaos.FloquetEvolution.projStep_transProbPreserving {N : ℕ} (F : FloquetEvolution (EuclideanSpace ℂ (Fin N))) : Projectivization.TransProbPreserving F.projStep

The one-period ray dynamics preserves transition probabilities — the hypothesis wigner_rigidity consumes.

theorem QuantumChaos.FloquetEvolution.projIterate_transProbPreserving {N : ℕ} (F : FloquetEvolution (EuclideanSpace ℂ (Fin N))) (n : ℕ) : Projectivization.TransProbPreserving (F.projIterate n)

The n-period ray dynamics preserves transition probabilities.

Inhabitation and the matrix-dynamics adapter seam

noncomputable def QuantumChaos.FloquetEvolution.refl (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℂ H] : FloquetEvolution H

The free (identity) evolution: inhabitation of the interface over any state space.

Equations

• QuantumChaos.FloquetEvolution.refl H = { step := 1 }

theorem QuantumChaos.inner_toEuclideanLin_unitary' {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) (v w : EuclideanSpace ℂ n) : inner ℂ ((Matrix.toEuclideanLin ↑U) v) ((Matrix.toEuclideanLin ↑U) w) = inner ℂ v w

Unitary inner-product preservation on EuclideanSpace ℂ n for an ARBITRARY finite index type: ⟪U v, U w⟫ = ⟪v, w⟫. Index-generic sibling of the staged Fin-N inner_toEuclideanLin_unitary (same proof recipe; fold into the staging tree when the rule of two fires — ⚠️ RESIDUE(R-014)). Needed because composite systems index by product types (Fin 2 × Fin 2 for two qubits).

noncomputable def QuantumChaos.FloquetEvolution.ofUnitaryMatrix {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) : FloquetEvolution (EuclideanSpace ℂ n)

The generic matrix-dynamics adapter: one period generated by a unitary matrix over ANY finite index type (composite systems index by product types, e.g. Fin 2 × Fin 2 for the kicked-Ising pilot). Same recipe as the staged Fin-N toEuclideanLinearEquiv: forward/inverse are toEuclideanLin of the matrix and its star, the round trips are the unitary relations, and the isometry is inner_toEuclideanLin_unitary'.

Equations

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

@[simp]

theorem QuantumChaos.FloquetEvolution.ofUnitaryMatrix_step_apply {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) (ψ : EuclideanSpace ℂ n) : (ofUnitaryMatrix U).step ψ = (Matrix.toEuclideanLin ↑U) ψ

noncomputable def QuantumChaos.FloquetEvolution.ofUnitary {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : FloquetEvolution (EuclideanSpace ℂ (Fin N))

The matrix-dynamics adapter: one period generated by a unitary matrix on ℂ^N. Kicked models (kicked Ising, kicked rotor) are products of such steps, so this seam is what the §H3 pilot instantiates; a future Physlib adapter replaces it without touching downstream theorems.

Equations

• QuantumChaos.FloquetEvolution.ofUnitary U = { step := let __src := Matrix.UnitaryGroup.toEuclideanLinearEquiv U; { toLinearEquiv := __src, norm_map' := ⋯ } }

@[simp]

theorem QuantumChaos.FloquetEvolution.ofUnitary_step_apply {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (ψ : EuclideanSpace ℂ (Fin N)) : (ofUnitary U).step ψ = (Matrix.toEuclideanLin ↑U) ψ