Chaos diagnostics: the out-of-time-order commutator (§H)

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

The third chaos diagnostic: the OTOC in commutator-norm form,

C(n) = ‖[A(n), B]‖, A(n) = (Uⁿ)† A (Uⁿ),

the growth of the commutator between a Heisenberg-evolved observable and a static one. Scrambling is C(n) becoming large for initially commuting A, B; the state-resolved form ⟨[A(n),B]†[A(n),B]⟩ is a refinement over this operator-norm envelope, not stated here.

• heisenberg U A = U† A U — Heisenberg conjugation over any finite index (the CV-6 CSD.CV.heisenberg is the FieldConfig instance, definitional bridge in CV/ChaosBounds.lean).
• otoc — the commutator-norm diagnostic; otoc_eq_zero_iff (vanishing = exact commutation), otoc_le (the a-priori envelope ≤ 2‖A‖‖B‖: conjugation by unitaries never grows the norm).

The teeth are in the instantiation: for the CV interacting drive the coupling-graph light cone forces otoc = 0 until the evolving observable's cone reaches the static probe's support (CV/ChaosBounds.lean, otoc_graphInteractingU_eq_zero) — scrambling provably cannot begin before causal contact. Honest scope: no exponential-growth (Lyapunov) claims; growth rates are the thread's recorded continuation.

noncomputable def QuantumChaos.heisenberg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (A : Matrix ι ι ℂ) : Matrix ι ι ℂ

Heisenberg conjugation over any finite index: A ↦ U† A U.

Equations

• QuantumChaos.heisenberg U A = star ↑U * A * ↑U

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

The OTOC, commutator-norm form: ‖[A(n), B]‖ with A(n) = (Uⁿ)† A (Uⁿ).

Equations

• QuantumChaos.otoc U A B n = ‖QuantumChaos.heisenberg (U ^ n) A * B - B * QuantumChaos.heisenberg (U ^ n) A‖

theorem QuantumChaos.otoc_eq_zero_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (A B : Matrix ι ι ℂ) (n : ℕ) : otoc U A B n = 0 ↔ heisenberg (U ^ n) A * B = B * heisenberg (U ^ n) A

The OTOC vanishes exactly when the evolved observable still commutes with the probe.

theorem QuantumChaos.l2_opNorm_heisenberg_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (A : Matrix ι ι ℂ) : ‖heisenberg U A‖ ≤ ‖A‖

Conjugation by a unitary never grows the L2 operator norm.

theorem QuantumChaos.otoc_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (A B : Matrix ι ι ℂ) (n : ℕ) : otoc U A B n ≤ 2 * ‖A‖ * ‖B‖

The a-priori OTOC envelope: C(n) ≤ 2‖A‖‖B‖ at every period — scrambling is bounded by the observables themselves.