Record persistence under post-record Floquet evolution (H3)

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

The "preserves a formed record when the record sector is invariant" clause of the §H3 pilot. Setting: after a record has formed, the arena factors as system × record, and post-record evolution that does not couple to the record factor acts as Φ ×ˢ id. Then:

• record_cylinder_invariant — every record cylinder (an event read off the record factor alone) is set-invariant: (Φ ×ˢ id)⁻¹ R = R. Not merely measure-preserved: the event is literally the same set, so the record persists surely, not just almost surely.
• record_cylinder_iterate_invariant — the same for every period count.
• prodMap_iterate — (Φ ×ˢ id)^[n] = Φ^[n] ×ˢ id (the record factor stays untouched for all time).
• floquetRecordStep_* — the CSD instantiation on (KSigma N) × Rec: the Floquet ontic step extended by the identity on a record factor is measure-preserving for kMuL ⊗ ν and leaves every record cylinder invariant at every period.

The stated hypothesis is the product form — the post-record dynamics does not couple to the record sector. That is exactly the regime the corpus's record modules call persistence (cf. SigmaLayer/RecordPersistence.lean, SigmaLayer/KSigmaRecord.lean: there records persist under the protocol's own dynamics; here under arbitrary post-record Floquet driving of the system factor). Coupled post-record dynamics — where the drive can erase records — is the §H thread's genuinely open continuation, priced by collapse_accuracy_bound-style results, and is deliberately out of the pilot.

def CSD.Empirical.QuantumChaos.postRecordStep {X : Type u_1} {R : Type u_2} (f : X → X) : X × R → X × R

Post-record evolution that does not couple to the record factor.

Equations

• CSD.Empirical.QuantumChaos.postRecordStep f = Prod.map f id

theorem CSD.Empirical.QuantumChaos.prodMap_iterate {X : Type u_1} {R : Type u_2} (f : X → X) (n : ℕ) : (postRecordStep f)^[n] = postRecordStep f^[n]

(f ×ˢ id)^[n] = f^[n] ×ˢ id: the record factor stays untouched for all time.

theorem CSD.Empirical.QuantumChaos.record_cylinder_invariant {X : Type u_1} {R : Type u_2} (f : X → X) (S : Set R) : postRecordStep f ⁻¹' Prod.snd ⁻¹' S = Prod.snd ⁻¹' S

★ Record cylinders are set-invariant under uncoupled post-record evolution: the record event is literally the same set after the step.

theorem CSD.Empirical.QuantumChaos.record_cylinder_iterate_invariant {X : Type u_1} {R : Type u_2} (f : X → X) (S : Set R) (n : ℕ) : (postRecordStep f)^[n] ⁻¹' Prod.snd ⁻¹' S = Prod.snd ⁻¹' S

★ Record cylinders are set-invariant at every period count.

theorem CSD.Empirical.QuantumChaos.postRecordStep_measurePreserving {X : Type u_1} {R : Type u_2} [MeasurableSpace X] [MeasurableSpace R] {f : X → X} {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hf : MeasureTheory.MeasurePreserving f μ μ) (ν : MeasureTheory.Measure R) [MeasureTheory.SFinite ν] : MeasureTheory.MeasurePreserving (postRecordStep f) (μ.prod ν) (μ.prod ν)

Uncoupled post-record evolution preserves any product measure whose system marginal the step preserves.

The CSD instantiation: Floquet driving after a record has formed

noncomputable def CSD.Empirical.QuantumChaos.floquetRecordStep {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (Rec : Type u_1) : LF4.KSigma N × Rec → LF4.KSigma N × Rec

The Floquet ontic step extended to a record-carrying arena (KSigma N) × Rec, acting trivially on the record factor.

Equations

• CSD.Empirical.QuantumChaos.floquetRecordStep U Rec = CSD.Empirical.QuantumChaos.postRecordStep (CSD.Empirical.QuantumChaos.floquetOnticStep U)

theorem CSD.Empirical.QuantumChaos.floquetRecordStep_measurePreserving {N : ℕ} [NeZero N] (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) {Rec : Type u_1} [MeasurableSpace Rec] (ν : MeasureTheory.Measure Rec) [MeasureTheory.SFinite ν] : MeasureTheory.MeasurePreserving (floquetRecordStep U Rec) ((LF4.kMuL p₀).prod ν) ((LF4.kMuL p₀).prod ν)

The record-extended Floquet step preserves kMuL ⊗ ν.

theorem CSD.Empirical.QuantumChaos.floquetRecordStep_record_invariant {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) {Rec : Type u_1} (S : Set Rec) (n : ℕ) : (floquetRecordStep U Rec)^[n] ⁻¹' Prod.snd ⁻¹' S = Prod.snd ⁻¹' S

★ Records persist under post-record Floquet driving: every record cylinder is the same set at every period count.