Documentation

CsdLean4.Incubator.QuantumChaos.SpectralFormFactor

Chaos diagnostics: the spectral form factor (quantum-chaos workstream, §H) #

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

The second chaos diagnostic behind the interface: the spectral form factor

SFF(n) = |Tr(Uⁿ)|² / N²,

the normalized modulus-squared trace of the n-period propagator — the standard probe of spectral statistics (its time profile distinguishes Poissonian from random-matrix level correlations).

What is delivered at this level is the object and its exact structure, not RMT statistics: sff is well-defined from the unitary alone, normalized (sff_zero), bounded (sff_le_one — every entry of a unitary power is bounded by the operator norm 1, via the staged Matrix.norm_entry_le_l2_opNorm), basis-independent (sff_conj — conjugation invariance, so the diagnostic is a property of the dynamics, not a matrix presentation), and explicitly computable for diagonal drives (sff_diagonal — the exponential-sum form; the free field's SFF is an instance, CV/ChaosBounds.lean).

The CSD reading, as for the Loschmidt echo: the propagator preserves every global overlap exactly, so SFF structure never signals information loss — it is a fingerprint of where the preserved information sits in the spectrum. Honest scope: no random-matrix or level-statistics claims; those are the thread's recorded continuation, not stated here.

source
noncomputable def QuantumChaos.sff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (n : ℕ) :
ℝ

The spectral form factor: the normalized modulus-squared trace of the n-period propagator, |Tr(Uⁿ)|² / N².

Equations
Instances For
    source
    @[simp]
    theorem QuantumChaos.sff_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) :
    sff U 0 = 1

    At n = 0 the form factor is exactly 1 — the normalization.

    source
    theorem QuantumChaos.sff_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (n : ℕ) :
    0 ≤ sff U n

    The form factor is nonnegative.

    source
    theorem QuantumChaos.sff_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (n : ℕ) :
    sff U n ≤ 1

    ★ The form factor is at most 1: every entry of a unitary power is bounded by the operator norm 1, so the trace is at most N.

    source
    theorem QuantumChaos.sff_conj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (V U : ↥(Matrix.unitaryGroup ι ℂ)) (n : ℕ) :
    sff (V * U * V⁻¹) n = sff U n

    ★ Basis independence: the form factor is conjugation-invariant — a property of the dynamics, not of a matrix presentation.

    source
    theorem QuantumChaos.sff_diagonal {ι : Type u_1} [Fintype ι] [DecidableEq ι] {u : ι → ℂ} {U : ↥(Matrix.unitaryGroup ι ℂ)} (hU : ↑U = Matrix.diagonal u) (n : ℕ) :
    sff U n = ‖∑ x : ι, u x ^ n‖ ^ 2 / ↑(Fintype.card ι) ^ 2

    The diagonal (integrable) case is an explicit exponential sum: Tr(Uⁿ) = ∑ₓ (u x)ⁿ for a diagonal drive. The free field's SFF is an instance (CV/ChaosBounds.lean).