Chaos diagnostics meet Stage 3: the light-cone gate and the echo price

Category: CV (continuous variables — the multi-mode field).

The §H diagnostics (Diagnostics, EchoBound, Otoc, SpectralFormFactor) instantiated on the Stage-3 interacting field, where the CV structure turns a-priori envelopes into sharp structural statements:

• ★★ otoc_graphInteractingU_eq_zero — the OTOC light-cone gate: for A supported on R and a static probe B supported on T, the out-of-time-order commutator is EXACTLY zero at every period n for which the coupling graph's n-ball of R is still disjoint from T. Scrambling cannot begin before A's light cone reaches the probe — the CV-8 cone re-expressed as the standard chaos diagnostic.
• ★★ one_sub_loschmidtEcho_interacting_le — the echo price: Loschmidt decay between the free and interacting drives is at most 2n·|τ|·|λ|·C — linear in period count and coupling, with the CV-9 Duhamel price as the per-period rate. The third linear-pricing rhyme (records: μ ≤ n·ε; locality: 2|τ||λ|C‖A‖; echo: 2n|τ||λ|C).
• sff_freeFieldU — the free field's spectral form factor as an explicit exponential sum over configurations: the integrable-case baseline that chaotic drives are diagnosed against.
• heisenberg_eq_chaos — the definitional bridge between the CV-6 Heisenberg conjugation and the interface-level one (same formula, one seam).

Honest scope: the gate is exact but one-directional (no claim the OTOC grows once the cones touch); the echo bound is an upper bound on decay; no random-matrix or Lyapunov-rate statements — growth rates and level statistics are the §H thread's recorded continuation.

References

CV/SupportSpreading.lean (CV-8, the cone); CV/InteractionPrice.lean (CV-9, the price); Incubator/QuantumChaos/{Diagnostics,EchoBound,Otoc,SpectralFormFactor}.lean; specs/external-library-map.md §H; specs/future-work.md.

theorem CSD.CV.heisenberg_eq_chaos {K N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : heisenberg U A = QuantumChaos.heisenberg U A

The CV-6 Heisenberg conjugation and the interface-level one agree definitionally.

theorem CSD.CV.otoc_graphInteractingU_eq_zero {K N : ℕ} {R T : Finset (Fin K)} {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (τ lam : ℝ) (E : Finset (Fin K × Fin K)) (g : Fin K × Fin K → Fin N → Fin N → ℝ) (n : ℕ) (hRT : Disjoint (graphBall E R n) T) (hA : SupportedOn R A) (hB : SupportedOn T B) : QuantumChaos.otoc (graphInteractingU K N τ lam E g) A B n = 0

★★ The OTOC light-cone gate: for A supported on R and a static probe B supported on T, the out-of-time-order commutator vanishes EXACTLY at every period for which the coupling graph's n-ball of R is still disjoint from T — scrambling cannot begin before A's light cone reaches the probe.

theorem CSD.CV.one_sub_loschmidtEcho_interacting_le {K N : ℕ} [NeZero N] (τ lam : ℝ) (v : FieldConfig K N → ℝ) {C : ℝ} (hC : 0 ≤ C) (hv : ∀ (c : FieldConfig K N), |v c| ≤ C) {ψ : FieldSpace K N} (hψ : ‖ψ‖ = 1) (n : ℕ) : 1 - QuantumChaos.loschmidtEcho (freeFieldFloquet K N τ) (interactingFloquet K N τ lam v) ψ n ≤ 2 * (↑n * (|τ| * (|lam| * C)))

★★ The echo price: Loschmidt decay between the free and the interacting drive is at most 2n·|τ|·|λ|·C — linear in period count and coupling, at the CV-9 Duhamel rate.

theorem CSD.CV.sff_freeFieldU (K N : ℕ) (τ : ℝ) (n : ℕ) : QuantumChaos.sff (freeFieldU K N τ) n = ‖∑ c : FieldConfig K N, Complex.exp (-(Complex.I * ↑(τ * fieldEnergy c))) ^ n‖ ^ 2 / ↑(Fintype.card (FieldConfig K N)) ^ 2

The free field's spectral form factor is an explicit exponential sum over configurations — the integrable baseline.

Q3: diagnostics beyond the gate — slow scrambling, exact revival

The OTOC gate above says scrambling cannot begin before the light cone arrives. The two results below complete the diagnostics pair (specs/BACKLOG.md §Q Q3): once the cone does arrive, scrambling in the kicked-diagonal family grows at most linearly — there is no fast scrambling in this model — and the free field's spectral form factor shows exact periodic revivals, the clean integrable signature against which chaotic ramps would be measured.

theorem CSD.CV.otoc_interactingU_le {K N : ℕ} [NeZero N] {R T : Finset (Fin K)} (hRT : Disjoint R T) (τ lam : ℝ) (v : FieldConfig K N → ℝ) {C : ℝ} (hC : 0 ≤ C) (hv : ∀ (c : FieldConfig K N), |v c| ≤ C) {A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) (hB : SupportedOn T B) (n : ℕ) : QuantumChaos.otoc (interactingU K N τ lam v) A B n ≤ 4 * ↑n * (|τ| * (|lam| * C)) * ‖A‖ * ‖B‖

★★ Slow scrambling — the OTOC growth cap. For disjointly supported observable and probe, the out-of-time-order commutator after n interacting periods is at most 4n·|τ|·|λ|·C·‖A‖·‖B‖: linear in period count at the Duhamel rate. The free evolution keeps A on its support (so the OTOC is zero along the free comparison), and the interacting evolution differs from it by at most the telescoped drive distance — scrambling in the kicked-diagonal family is at most linear, never exponential.

theorem CSD.CV.freeField_phase_two_pi (K N : ℕ) (c : FieldConfig K N) : Complex.exp (-(Complex.I * ↑(2 * Real.pi * fieldEnergy c))) = Complex.exp (-(Complex.I * ↑Real.pi * ↑K))

The free field's phases all coincide at τ = 2π: the spectrum is integer-spaced (oscEnergy n = n + ½), so 2π·E(c) ≡ πK (mod 2π) for every configuration.

theorem CSD.CV.sff_freeFieldU_revival (K N : ℕ) [NeZero N] (n : ℕ) : QuantumChaos.sff (freeFieldU K N (2 * Real.pi)) n = 1

★ Exact revival — the integrable signature. At τ = 2π the free field's spectral form factor is exactly 1 at every period count: all phases coincide, the trace never decays, and the SFF shows none of the dip–ramp–plateau structure of a scrambling system. The clean baseline the OTOC cap above is measured against.