The small-coupling witness: the half-life bound bites (§H continuation)

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

RecordDegradation.lean priced coupled post-record driving by the record half-life bound μ (intact n)ᶜ ≤ n · ε. This module shows the bound is not vacuous: a concrete weakly coupled drive with coupling strength strictly between 0 and 1.

• triggeredRecordKick F C δ — the drive: the system evolves by F; the record (a circle coordinate) is kicked by δ exactly when the system lies in the trigger region C. Measure-preserving whenever F is, by the skew-product theorem (each record slice is a rotation).
• recordFlip_triggeredRecordKick — for δ ≠ 0 the coupling set IS the trigger cylinder C ×ˢ univ, so the coupling strength is exactly μ C: the geometry of the trigger region is the record-degradation rate.
• ★ fibreTriggeredKick and its lemmas — the CSD instantiation on (KSigma N) × S¹: the trigger is a fibre-arc cylinder (first torus angle in a quarter-radius ball), giving coupling strength exactly 1/2 (AddCircle.volume_closedBall): 0 < ε < 1, and the half-life bound reads "a formed record survives n periods of this drive except on measure at most n/2" — a bound that genuinely bites.

Honest scope: the witness shows the PRICE is non-trivial; whether the bound is attained (actual erasure rate) is a dynamics question beyond the pilot, sitting with the thread's diagnostics work. Cross-references: specs/external-library-map.md §H, specs/future-work.md.

The triggered record kick, generically

@[reducible, inline]

abbrev CSD.Empirical.QuantumChaos.RecordCircle : Type

The circle-valued record coordinate.

Equations

• CSD.Empirical.QuantumChaos.RecordCircle = AddCircle 1

noncomputable def CSD.Empirical.QuantumChaos.triggeredRecordKick {A : Type u_1} (F : A → A) (C : Set A) (δ : RecordCircle) : A × RecordCircle → A × RecordCircle

The triggered record kick: the system evolves by F; the record is kicked by δ exactly when the system lies in the trigger region C.

Equations

• CSD.Empirical.QuantumChaos.triggeredRecordKick F C δ x = (F x.1, x.2 + if x.1 ∈ C then δ else 0)

theorem CSD.Empirical.QuantumChaos.triggeredRecordKick_measurePreserving {A : Type u_1} [MeasurableSpace A] {F : A → A} {μ : MeasureTheory.Measure A} [MeasureTheory.SFinite μ] (hF : MeasureTheory.MeasurePreserving F μ μ) {C : Set A} (hC : MeasurableSet C) (δ : RecordCircle) : MeasureTheory.MeasurePreserving (triggeredRecordKick F C δ) (μ.prod MeasureTheory.volume) (μ.prod MeasureTheory.volume)

The triggered kick is measure-preserving whenever the system step is: skew product with rotation slices.

theorem CSD.Empirical.QuantumChaos.recordFlip_triggeredRecordKick {A : Type u_1} (F : A → A) (C : Set A) {δ : RecordCircle} (hδ : δ ≠ 0) : recordFlip (triggeredRecordKick F C δ) Prod.snd = C ×ˢ Set.univ

For δ ≠ 0 the coupling set of the triggered kick is exactly the trigger cylinder: the trigger geometry IS the coupling.

theorem CSD.Empirical.QuantumChaos.measure_recordFlip_triggeredRecordKick {A : Type u_1} [MeasurableSpace A] (F : A → A) {μ : MeasureTheory.Measure A} (C : Set A) {δ : RecordCircle} (hδ : δ ≠ 0) : (μ.prod MeasureTheory.volume) (recordFlip (triggeredRecordKick F C δ) Prod.snd) = μ C

The coupling strength of the triggered kick is the trigger region's measure.

The CSD instantiation: a fibre-triggered kick with ε = 1/2

noncomputable def CSD.Empirical.QuantumChaos.fibreTrigger (N : ℕ) : Set (LF4.KSigma N)

The fibre-arc trigger: the first torus angle lies within a quarter radius of 0. A context-style region read off the ontic fibre alone.

Equations

• CSD.Empirical.QuantumChaos.fibreTrigger N = {x : CSD.LF4.KSigma N | x.2.1 ∈ Metric.closedBall 0 (1 / 4)}

theorem CSD.Empirical.QuantumChaos.fibreTrigger_measurableSet {N : ℕ} : MeasurableSet (fibreTrigger N)

theorem CSD.Empirical.QuantumChaos.kMuL_fibreTrigger {N : ℕ} [NeZero N] (p₀ : LF4.CPN N) : (LF4.kMuL p₀) (fibreTrigger N) = ENNReal.ofReal (1 / 2)

The trigger's Liouville measure is exactly 1/2: vol(closedBall 0 (1/4)) = min 1 (2·(1/4)) = 1/2 on the unit circle.

noncomputable def CSD.Empirical.QuantumChaos.fibreTriggeredKick {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (δ : RecordCircle) : LF4.KSigma N × RecordCircle → LF4.KSigma N × RecordCircle

The fibre-triggered kick: the Floquet ontic step, with the record kicked whenever the first fibre angle lies in the quarter-ball arc.

Equations

• CSD.Empirical.QuantumChaos.fibreTriggeredKick U δ = CSD.Empirical.QuantumChaos.triggeredRecordKick (CSD.Empirical.QuantumChaos.floquetOnticStep U) (CSD.Empirical.QuantumChaos.fibreTrigger N) δ

theorem CSD.Empirical.QuantumChaos.fibreTriggeredKick_measurePreserving {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) (δ : RecordCircle) : MeasureTheory.MeasurePreserving (fibreTriggeredKick U δ) ((LF4.kMuL p₀).prod MeasureTheory.volume) ((LF4.kMuL p₀).prod MeasureTheory.volume)

The fibre-triggered kick preserves kMuL ⊗ vol.

theorem CSD.Empirical.QuantumChaos.fibreTriggeredKick_coupling {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) {δ : RecordCircle} (hδ : δ ≠ 0) : ((LF4.kMuL p₀).prod MeasureTheory.volume) (recordFlip (fibreTriggeredKick U δ) Prod.snd) = ENNReal.ofReal (1 / 2)

★ The coupling strength is exactly 1/2 — strictly between 0 and 1: the half-life bound genuinely bites.

theorem CSD.Empirical.QuantumChaos.fibreTriggeredKick_record_halfLife {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) {δ : RecordCircle} (hδ : δ ≠ 0) (n : ℕ) : ((LF4.kMuL p₀).prod MeasureTheory.volume) (recordIntact (fibreTriggeredKick U δ) Prod.snd n)ᶜ ≤ n • ENNReal.ofReal (1 / 2)

★ The half-life bound, bitten: under the fibre-triggered kick a formed record survives n periods except on measure at most n/2.