The half-life bound is attained (§H continuation: attainment)

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

RecordDegradation.lean priced coupled driving by μ (intact n)ᶜ ≤ n • ε and CouplingWitness.lean showed the bound bites (ε = 1/2). This module closes the remaining question: is the linear rate real, or is the bound loose? Answer: it is attained with equality.

The witness is the cyclic-shift kick: the base is the uniform cycle Fin m under x ↦ x + 1, and the record coordinate is kicked exactly when the base sits at 0. Two structural facts make the analysis exact: within any window of n ≤ m periods every trajectory visits the trigger at most once (the shift is a cycle), and a single visit flips the readout permanently within the window. Hence:

• cyclicKick_iterate — the closed-form trajectory (base advances, the record accumulates the visit indicators);
• recordIntact_compl_cyclicKick — the unstable set is EXACTLY the cylinder over the n base points that reach the trigger within the window (set equality, not an estimate);
• ★★ cyclicKick_halfLife_attained — on the window n ≤ m, μ (intact n)ᶜ = n • ε with ε = 1/m: the record half-life bound is an equality for the cyclic kick — linear degradation at exactly the coupling rate is realised, so the generic bound is sharp.

Honest scope: attainment on the window n ≤ m (after a full cycle the second visit un-flips a δ of order two and the count saturates — correctly so, since n • ε exceeds 1 there while measures cannot); sharpness is exhibited for this drive, with no claim that every drive attains its bound. Cross-references: specs/external-library-map.md §H, specs/future-work.md.

The cyclic-shift kick

def CSD.Empirical.QuantumChaos.cyclicShift (m : ℕ) [NeZero m] : Fin m → Fin m

The base dynamics: the uniform cycle on Fin m.

Equations

• CSD.Empirical.QuantumChaos.cyclicShift m x = x + 1

noncomputable def CSD.Empirical.QuantumChaos.uniformFin (m : ℕ) : MeasureTheory.Measure (Fin m)

The uniform probability measure on the cycle.

Equations

• CSD.Empirical.QuantumChaos.uniformFin m = (↑m)⁻¹ • MeasureTheory.Measure.count

noncomputable def CSD.Empirical.QuantumChaos.cyclicKick (m : ℕ) [NeZero m] (δ : RecordCircle) : Fin m × RecordCircle → Fin m × RecordCircle

The cyclic kick: the record is kicked exactly when the base sits at 0.

Equations

• CSD.Empirical.QuantumChaos.cyclicKick m δ = CSD.Empirical.QuantumChaos.triggeredRecordKick (CSD.Empirical.QuantumChaos.cyclicShift m) {0} δ

theorem CSD.Empirical.QuantumChaos.ofNat_val_of_lt {m : ℕ} [NeZero m] {j : ℕ} (h : j < m) : ↑(Fin.ofNat m j) = j

Fin.ofNat below one full cycle is faithful.

theorem CSD.Empirical.QuantumChaos.ofNat_succ {m : ℕ} [NeZero m] (k : ℕ) : Fin.ofNat m (k + 1) = Fin.ofNat m k + 1

Fin.ofNat respects the successor.

theorem CSD.Empirical.QuantumChaos.cyclicKick_iterate (m : ℕ) [NeZero m] (δ : RecordCircle) (x : Fin m) (r : RecordCircle) (k : ℕ) : (cyclicKick m δ)^[k] (x, r) = (x + Fin.ofNat m k, r + ∑ j ∈ Finset.range k, if x + Fin.ofNat m j = 0 then δ else 0)

The closed-form trajectory: the base advances one step per period and the record accumulates the trigger-visit indicators.

The unstable set, exactly

theorem CSD.Empirical.QuantumChaos.recordIntact_compl_cyclicKick {m : ℕ} [NeZero m] {δ : RecordCircle} (hδ : δ ≠ 0) {n : ℕ} (hn : n ≤ m) : (recordIntact (cyclicKick m δ) Prod.snd n)ᶜ = {x : Fin m | ∃ j < n, x + Fin.ofNat m j = 0} ×ˢ Set.univ

The unstable set is exactly the reach-the-trigger cylinder: on a window of at most one full cycle, a trajectory's readout changes iff its base reaches 0 within the window (set equality, not an estimate).

Attainment

theorem CSD.Empirical.QuantumChaos.count_reachSet {m : ℕ} [NeZero m] {n : ℕ} (hn : n ≤ m) : MeasureTheory.Measure.count {x : Fin m | ∃ j < n, x + Fin.ofNat m j = 0} = ↑n

The reach set has exactly n points on the window.

theorem CSD.Empirical.QuantumChaos.cyclicKick_halfLife_attained {m : ℕ} [NeZero m] {δ : RecordCircle} (hδ : δ ≠ 0) {n : ℕ} (hn : n ≤ m) : ((uniformFin m).prod MeasureTheory.volume) (recordIntact (cyclicKick m δ) Prod.snd n)ᶜ = n • ((uniformFin m).prod MeasureTheory.volume) (recordFlip (cyclicKick m δ) Prod.snd)

★★ The half-life bound is attained: on the window n ≤ m, the cyclic kick's unstable measure EQUALS n • ε with ε = 1/m the coupling strength — linear record degradation at exactly the coupling rate is realised, so the generic bound recordIntact_compl_measure_le is sharp.