Documentation

CsdLean4.Incubator.QuantumChaos.Diagnostics

Chaos diagnostics: the Loschmidt echo (quantum-chaos workstream, §H) #

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

The first chaos diagnostic behind the interface (class 3 of the map's rule: verified missing in Physlib 2026-08-07): the Loschmidt echo

L(n) = ‖⟨ψ, (F₂ⁿ)⁻¹ F₁ⁿ ψ⟩‖² = ‖⟨F₂ⁿ ψ, F₁ⁿ ψ⟩‖²,

the fidelity between evolving ψ for n periods under F₁ versus under a perturbed drive F₂. Sensitivity of L(n) to the perturbation is the standard dynamical-instability diagnostic.

The CSD reading, fixed by the interface's information-preservation lemmas: BOTH evolutions preserve every global overlap exactly (inner_iterate_iterate), so echo decay never signals information loss — it measures the divergence of two informationally lossless evolutions, i.e. where the preserved information has been relocated. That is scrambling as relocation, the reading the ontic layer makes literal (records and accessibility live in Empirical/CSD/QuantumChaos/).

API: loschmidtEcho, endpoint values (loschmidtEcho_zero, loschmidtEcho_self), the unit-interval bounds (loschmidtEcho_nonneg, loschmidtEcho_le_one via Cauchy–Schwarz + isometry), and symmetry (loschmidtEcho_comm).

source
noncomputable def QuantumChaos.loschmidtEcho {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F₁ F₂ : FloquetEvolution H) (ψ : H) (n : ℕ) :
ℝ

The Loschmidt echo: the fidelity after n periods between the drive F₁ and the perturbed drive F₂, from the state ψ.

Equations
Instances For
    source
    @[simp]
    theorem QuantumChaos.loschmidtEcho_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F₁ F₂ : FloquetEvolution H) {ψ : H} (hψ : ‖ψ‖ = 1) :
    loschmidtEcho F₁ F₂ ψ 0 = 1

    At n = 0 the echo is the squared norm (= 1 on unit states).

    source
    @[simp]
    theorem QuantumChaos.loschmidtEcho_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F : FloquetEvolution H) {ψ : H} (hψ : ‖ψ‖ = 1) (n : ℕ) :
    loschmidtEcho F F ψ n = 1

    The unperturbed echo is 1 at every period count: evolving twice the same way never decays.

    source
    theorem QuantumChaos.loschmidtEcho_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F₁ F₂ : FloquetEvolution H) (ψ : H) (n : ℕ) :
    0 ≤ loschmidtEcho F₁ F₂ ψ n

    The echo is nonnegative.

    source
    theorem QuantumChaos.loschmidtEcho_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F₁ F₂ : FloquetEvolution H) {ψ : H} (hψ : ‖ψ‖ = 1) (n : ℕ) :
    loschmidtEcho F₁ F₂ ψ n ≤ 1

    The echo is at most 1 on unit states: Cauchy–Schwarz, with both evolutions norm-preserving.

    source
    theorem QuantumChaos.loschmidtEcho_comm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (F₁ F₂ : FloquetEvolution H) (ψ : H) (n : ℕ) :
    loschmidtEcho F₁ F₂ ψ n = loschmidtEcho F₂ F₁ ψ n

    The echo is symmetric in the two drives (conjugate-symmetry of the inner product).