The echo-perturbation bound: Loschmidt decay is priced by drive distance

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

The quantitative link between the Loschmidt echo and the operator distance of the two drives:

1 − L(n) ≤ 2·n·‖U − W‖.

• norm_toEuclideanLin_apply_le — the action bound ‖M·ψ‖ ≤ ‖M‖·‖ψ‖ (L2 operator norm; definitionally l2_opNorm_mulVec).
• norm_iterate_sub_iterate_le — the telescoping perturbation bound for the matrix adapter: ‖Uⁿψ − Wⁿψ‖ ≤ n·‖U − W‖·‖ψ‖ (each step splits into an isometry factor and one fresh U − W action).
• ★ one_sub_loschmidtEcho_le — the echo bound: on unit states, 1 − L(n) ≤ 2·(n·‖U − W‖), via 1 − |z|² ≤ 2|1 − z| and 1 − z = ⟨Wⁿψ, (Wⁿ − Uⁿ)ψ⟩.

Echo decay is at most linear in period count and drive distance — the diagnostics-side rhyme of the record half-life bound μ ≤ n·ε and of the CV pricing ladder: instantiated on the interacting field (CV/ChaosBounds.lean), the drive distance is the CV-9 Duhamel price, so echo decay is bounded by 2n·|τ|·|λ|·C. Honest scope: an upper bound on the decay — no claim the echo actually decays at this (or any) rate.

theorem QuantumChaos.norm_toEuclideanLin_apply_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℂ) (v : EuclideanSpace ℂ ι) : ‖(Matrix.toEuclideanLin M) v‖ ≤ ‖M‖ * ‖v‖

The action of a matrix on a Euclidean vector is bounded by its L2 operator norm (definitionally l2_opNorm_mulVec).

theorem QuantumChaos.norm_iterate_sub_iterate_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U W : ↥(Matrix.unitaryGroup ι ℂ)) (n : ℕ) (ψ : EuclideanSpace ℂ ι) : ‖((FloquetEvolution.ofUnitaryMatrix U).iterate n) ψ - ((FloquetEvolution.ofUnitaryMatrix W).iterate n) ψ‖ ≤ ↑n * ‖↑U - ↑W‖ * ‖ψ‖

The telescoping perturbation bound: iterating two matrix drives from the same state separates at most linearly, one fresh U − W action per period (the other factor is an isometry).

theorem QuantumChaos.one_sub_loschmidtEcho_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U W : ↥(Matrix.unitaryGroup ι ℂ)) {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) (n : ℕ) : 1 - loschmidtEcho (FloquetEvolution.ofUnitaryMatrix U) (FloquetEvolution.ofUnitaryMatrix W) ψ n ≤ 2 * (↑n * ‖↑U - ↑W‖)

★ The echo-perturbation bound: on unit states, 1 − L(n) ≤ 2·(n·‖U − W‖) — Loschmidt decay is at most linear in period count and drive distance.