Record degradation under coupled post-record driving (§H continuation)

Category: 6-Empirical-CSD (the CSD reading of stroboscopic dynamics).

The pilot (RecordPersistence.lean) covered the UNCOUPLED regime: driving that does not touch the record factor preserves every record cylinder surely. This module prices the COUPLED regime — post-record driving that CAN move the record — with the record-half-life bound.

The right degradation quantity

For a measure-preserving coupled step Φ, the bare probability of a record event never changes (μ (Φ⁻¹ R) = μ R is exactly measure preservation), so "the record probability decays" is NOT the honest statement. What degrades is stability: whether the trajectory's readout still shows the original value. Accordingly:

• recordFlip Φ ρ — the per-step coupling set: points whose readout ρ changes in one step. Its measure ε := μ (recordFlip Φ ρ) is the coupling strength.
• recordIntact Φ ρ n — trajectories whose readout survives n periods unchanged.
• exists_flip_of_ne — a readout change within n periods forces a visit to the coupling set (the least-change argument, in induction form).
• ★★ recordIntact_compl_measure_le — the record half-life bound: μ (recordIntact Φ ρ n)ᶜ ≤ n • ε. A formed record survives n periods of coupled driving except on a set of measure at most n · ε — degradation is at most linear in time, at rate the per-step record-sector coupling.
• recordIntact_compl_null_of_flip_null — null coupling gives almost-sure persistence at every period count.
• recordFlip_postRecordStep / recordIntact_postRecordStep — the pilot recovered: uncoupled driving has EMPTY coupling set, and the half-life bound collapses to the pilot's sure persistence (ε = 0).
• floquetRecordStep_recordFlip — the CSD instantiation: the pilot's uncoupled Floquet record step has ε = 0; any measure-preserving coupled step on (KSigma N) × Rec is priced by the generic bound.

This is the discrete-time sibling of the record-erasure pricing the corpus carries elsewhere (collapse_accuracy_bound's spirit: touching records costs, and the cost is quantified). Honest scope: the bound is an inequality in the coupling measure, with no claim it is attained; exhibiting a small-coupling witness with 0 < ε < 1 (a weakly record-coupled drive) is the thread's next brick, recorded in BACKLOG §H. Cross-references: specs/external-library-map.md §H, specs/future-work.md.

def CSD.Empirical.QuantumChaos.recordFlip {A : Type u_1} {V : Type u_2} (Φ : A → A) (ρ : A → V) : Set A

The per-step coupling set: points whose readout changes in one step. Empty exactly when the step does not couple to the record sector.

Equations

• CSD.Empirical.QuantumChaos.recordFlip Φ ρ = {a : A | ρ (Φ a) ≠ ρ a}

def CSD.Empirical.QuantumChaos.recordIntact {A : Type u_1} {V : Type u_2} (Φ : A → A) (ρ : A → V) (n : ℕ) : Set A

Trajectories whose readout survives n periods unchanged.

Equations

• CSD.Empirical.QuantumChaos.recordIntact Φ ρ n = {a : A | ∀ k ≤ n, ρ (Φ^[k] a) = ρ a}

theorem CSD.Empirical.QuantumChaos.exists_flip_of_ne {A : Type u_1} {V : Type u_2} {Φ : A → A} {ρ : A → V} {a : A} {k : ℕ} (hk : ρ (Φ^[k] a) ≠ ρ a) : ∃ j < k, Φ^[j] a ∈ recordFlip Φ ρ

A readout change within n steps forces a visit to the coupling set strictly earlier (the least-change argument, induction form).

theorem CSD.Empirical.QuantumChaos.compl_recordIntact_subset {A : Type u_1} {V : Type u_2} (Φ : A → A) (ρ : A → V) (n : ℕ) : (recordIntact Φ ρ n)ᶜ ⊆ ⋃ k ∈ Finset.range n, Φ^[k] ⁻¹' recordFlip Φ ρ

The unstable set is covered by the pulled-back coupling sets.

theorem CSD.Empirical.QuantumChaos.recordIntact_compl_measure_le {A : Type u_1} {V : Type u_2} [MeasurableSpace A] {μ : MeasureTheory.Measure A} {Φ : A → A} {ρ : A → V} (hΦ : MeasureTheory.MeasurePreserving Φ μ μ) (hD : MeasurableSet (recordFlip Φ ρ)) (n : ℕ) : μ (recordIntact Φ ρ n)ᶜ ≤ n • μ (recordFlip Φ ρ)

★★ The record half-life bound. Under a measure-preserving (possibly record-coupled) step, a formed record survives n periods except on a set of measure at most n · ε, where ε is the measure of the per-step coupling set: degradation is at most linear in time, at rate the record-sector coupling.

theorem CSD.Empirical.QuantumChaos.recordIntact_compl_null_of_flip_null {A : Type u_1} {V : Type u_2} [MeasurableSpace A] {μ : MeasureTheory.Measure A} {Φ : A → A} {ρ : A → V} (hΦ : MeasureTheory.MeasurePreserving Φ μ μ) (hD : MeasurableSet (recordFlip Φ ρ)) (h0 : μ (recordFlip Φ ρ) = 0) (n : ℕ) : μ (recordIntact Φ ρ n)ᶜ = 0

Null coupling gives almost-sure record persistence at every period count.

The uncoupled case: the pilot recovered as ε = 0

@[simp]

theorem CSD.Empirical.QuantumChaos.recordFlip_postRecordStep {X : Type u_1} {R : Type u_2} (f : X → X) : recordFlip (postRecordStep f) Prod.snd = ∅

Uncoupled driving has EMPTY coupling set: the readout never changes.

theorem CSD.Empirical.QuantumChaos.recordIntact_postRecordStep {X : Type u_1} {R : Type u_2} (f : X → X) (n : ℕ) : recordIntact (postRecordStep f) Prod.snd n = Set.univ

Under uncoupled driving every trajectory is record-intact at every period count — the pilot's sure persistence, recovered as the ε = 0 case of the half-life bound.

The CSD instantiation

@[simp]

theorem CSD.Empirical.QuantumChaos.floquetRecordStep_recordFlip {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (Rec : Type u_1) : recordFlip (floquetRecordStep U Rec) Prod.snd = ∅

The pilot's Floquet record step has zero coupling: ε = 0. Any measure-preserving COUPLED step on the same arena is priced by recordIntact_compl_measure_le instead.