SigmaLayer/UnifiedArena: the engine migration — operational content on the swap arena

Category: 7-SigmaLayer (the record layer — arena unification, step 2 of 2).

What this is

CsdFiniteQMClosure was honest that it conjoined an operational closure on productDynamics over ℂℙ^M × T² with a dynamical closure on the swap arena — "both hold", not "one theory covers both". This module ends that split for the rank-one projective tier: one arena carries the isolated Schrödinger dynamics AND the rank-one measurement dynamics AND Born AND rank-one Lüders AND mixed-state weights/frequencies. (Scope corrected 2026-08-02, second external review: the degenerate update lives on the companion projective-join witness (JoinLuders.lean), the any-basis closure is the separate RotatedSwapClosure, and mixed/POVM dynamics remain open — a single projective-measurement capstone bundling all of these is a recorded open item, specs/BACKLOG.md.)

The arena is UnifiedArena M = ((ℂℙ^M × T²) × T²_R) × (Fin (M+1) → Σ_sys) — system (base ray + system fibre), pointer register, calibrated ancilla bank. Its Liouville measure arenaLiouville = (kMuL ⊗ vol) ⊗ Π kMuL is swapMeasure at μs = kMuL p₀, so swapEvolve_measurePreserving already provides measurement-preservation against it — the measure the measurement dynamics preserves is the Liouville measure the isolated flow preserves. That coincidence is the engine migration's mathematical content.

The field mapping from FiniteQMClosure (all eleven accounted for)

operational field	fate on the unified arena
isolated_flow_measure_preserving	migrated — arenaIso (the lifted exp(-itH)) preserves arenaLiouville
schrodinger_projection	migrated — arenaRay ∘ arenaIso t = productProjectedFlow t ∘ arenaRay
fubini_study_bridge	migrated — (arenaRay)_* arenaLiouville = μ_FS
measurement_preserving	migrated & upgraded — the record-creating propagator swapEvolve preserves arenaLiouville (the operational field's de-isolation interaction did not create persistent records)
readout_ae_total, records_established, records_time_physical	superseded — the measurement field's record creation/persistence is context-fixed and dynamical, strictly stronger than the preparation-indexed vnPointerOutcome readout (the MD-1 repair)
born_frequency	migrated — same i.i.d. LLN, trials sampling arenaLiouville, regions the arena cylinders of the Born regions
conditioning_is_luders	superseded — the measurement field's luders_followup is the dynamical Lüders update (collapse as pushforward), strictly stronger than conditioning-as-prediction
mixed_born	migrated — spectral mixtures of arena cylinder measures reproduce Tr(ρEᵢ)
mixed_born_frequency	migrated (same day, second pass) — arena_mixed_born_frequency: the two-stage mixture LLN through the system-slot marginal, with arenaMixtureRegion a Prod.map preimage so the transfer is rfl-level

⚠️ Honest scope

• The isolated lift arenaIso acts by exp(-itH) on the system slot and identity on register and bank: the apparatus is idle between measurements, and the bank is re-calibrated per round (the calibration posit of SwapLuders.lean, unchanged).
• The propagator alternation — isolate, then measure, then isolate — is now a theorem (arena_round_trip, second pass same day): the record is created from the evolved state's selector and survives subsequent isolated evolution, because the pointer register is a conserved coordinate of the lifted flow (readout_arenaIso — definitional). The composition was not even stateable before the migration.
• Everything the predecessor capstones honestly scoped stays scoped: the piecewise-Hamiltonian classification of the measurement propagator (PiecewiseHamiltonian.lean), the calibration posit, rank-one first measurements.

References

SigmaLayer/FiniteQMClosure.lean (the operational predecessor, untouched); SigmaLayer/SwapClosure.lean (SwapMeasurementClosure — the dynamical half); SigmaLayer/MeasureBridge.lean (productDynamics, productSector, productSector_hasFubiniStudyPushforward); SigmaLayer/DynamicsBridge.lean (productDynamicsBridge.projectable); SigmaLayer/SwapWitness.lean (swapMeasure, swapEvolve_measurePreserving); SigmaLayer/UnifiedFlowedRecords.lean (unified_born_frequency); SigmaLayer/MixedOntic.lean (mixed_ontic_born_weight); specs/BACKLOG.md (the engine-migration row, closed by this module).

@[reducible, inline]

abbrev CSD.RecordLayer.UnifiedArena (M : ℕ) : Type

The unified arena: system (base ray + system fibre) × pointer register × calibrated ancilla bank — the one space carrying both the isolated Schrödinger dynamics and the measurement dynamics.

Equations

• CSD.RecordLayer.UnifiedArena M = CSD.RecordLayer.SwapArena (CSD.LF4.KSigma (M + 1)) (M + 1)

noncomputable def CSD.RecordLayer.arenaLiouville (M : ℕ) (p₀ : LF4.CPN (M + 1)) : MeasureTheory.Measure (UnifiedArena M)

The arena Liouville measure: Liouville on the system slot, Haar on the register, Liouville on every bank slot. This is swapMeasure at μs = kMuL p₀ — so the measurement propagator's measure-preservation theorem applies to it verbatim.

Equations

• CSD.RecordLayer.arenaLiouville M p₀ = CSD.RecordLayer.swapMeasure (CSD.LF4.kMuL p₀) (M + 1)

instance CSD.RecordLayer.instIsProbabilityMeasureUnifiedArenaArenaLiouville {M : ℕ} (p₀ : LF4.CPN (M + 1)) : MeasureTheory.IsProbabilityMeasure (arenaLiouville M p₀)

noncomputable def CSD.RecordLayer.arenaIso {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (t : ℝ) : UnifiedArena M → UnifiedArena M

The isolated flow, lifted to the arena: exp(-itH) on the system slot, identity on register and bank.

Equations

• CSD.RecordLayer.arenaIso H hH p₀ t x = (((CSD.SigmaLayer.productDynamics H hH p₀).flow t x.1.1, x.1.2), x.2)

noncomputable def CSD.RecordLayer.arenaRay {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) : UnifiedArena M → LF4.CPN (M + 1)

The ray projection of the arena: project the system slot to its base ray.

Equations

• CSD.RecordLayer.arenaRay H hH p₀ x = (CSD.SigmaLayer.productSector H hH p₀).pi x.1.1

Marginals

theorem CSD.RecordLayer.productDynamics_muL {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) : ↑(SigmaLayer.productDynamics H hH p₀).muL = LF4.kMuL p₀

The product model's Liouville measure is kMuL — the identification the migration rests on.

theorem CSD.RecordLayer.arenaLiouville_cylinder {M : ℕ} (p₀ : LF4.CPN (M + 1)) (S : Set (LF4.KSigma (M + 1))) : (arenaLiouville M p₀) ((fun (x : UnifiedArena M) => x.1.1) ⁻¹' S) = (LF4.kMuL p₀) S

Cylinder sets over the system slot carry exactly the system Liouville measure.

theorem CSD.RecordLayer.arenaLiouville_sys_marginal {M : ℕ} (p₀ : LF4.CPN (M + 1)) : MeasureTheory.Measure.map (fun (x : UnifiedArena M) => x.1.1) (arenaLiouville M p₀) = LF4.kMuL p₀

The system-slot marginal of the arena Liouville measure is the system Liouville measure.

The migrated isolated dynamics

theorem CSD.RecordLayer.arenaIso_measurePreserving {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (t : ℝ) : MeasureTheory.MeasurePreserving (arenaIso H hH p₀ t) (arenaLiouville M p₀) (arenaLiouville M p₀)

The lifted isolated flow preserves the arena Liouville measure.

theorem CSD.RecordLayer.arenaIso_schrodinger {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (t : ℝ) (x : UnifiedArena M) : arenaRay H hH p₀ (arenaIso H hH p₀ t x) = SigmaLayer.productProjectedFlow H hH t (arenaRay H hH p₀ x)

The lifted flow projects to Schrödinger evolution on rays — the Schrödinger pillar, on the unified arena.

theorem CSD.RecordLayer.arenaRay_pushforward {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) : MeasureTheory.Measure.map (arenaRay H hH p₀) (arenaLiouville M p₀) = Matrix.UnitaryGroup.fubiniStudyMeasure p₀

The Fubini–Study bridge, on the unified arena: the ray-projected law of the arena Liouville measure is the Fubini–Study measure.

The unified closure

structure CSD.RecordLayer.UnifiedArenaClosure {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) : Prop

★★ The unified-arena closure: one arena carries isolated dynamics and the complete rank-one projective measurement reconstruction. (Scope corrected 2026-08-02 — see the module header: degenerate Lüders lives on the join witness; a bundling capstone is recorded.)

The successor of CsdFiniteQMClosure's two-arena conjunction: every field is a statement about UnifiedArena M and its Liouville measure arenaLiouville. Isolated Schrödinger dynamics, Fubini–Study bridge, measurement dynamics (record creation, exclusivity, persistence, dynamical Born, rank-one Lüders), i.i.d. Born frequencies, and mixed-state Born weights — one arena, one measure family. The field mapping from the operational closure (migrated / upgraded / superseded / recorded) is the module header's table.

• isolated_flow_measure_preserving (t : ℝ) : MeasureTheory.MeasurePreserving (arenaIso H hH p₀ t) (arenaLiouville M p₀) (arenaLiouville M p₀)

  The lifted isolated flow preserves the arena Liouville measure.

• schrodinger_projection (t : ℝ) (x : UnifiedArena M) : arenaRay H hH p₀ (arenaIso H hH p₀ t x) = SigmaLayer.productProjectedFlow H hH t (arenaRay H hH p₀ x)

  The lifted flow projects to Schrödinger evolution exp(-itH) • · on rays.

• fubini_study_bridge : MeasureTheory.Measure.map (arenaRay H hH p₀) (arenaLiouville M p₀) = Matrix.UnitaryGroup.fubiniStudyMeasure p₀

  The ray-projected law of the arena Liouville measure is Fubini–Study (B1).

• measurement_preserving (s t : SigmaLayer.OnticTime) : MeasureTheory.MeasurePreserving (swapEvolve (basinIndex (momentContext (M + 1))) s t) (arenaLiouville M p₀) (arenaLiouville M p₀)

  The record-creating measurement propagator preserves the SAME Liouville measure.

• measurement : SwapMeasurementClosure (M + 1) ψ

  Measurement as a process on this arena: ready ⇒ no record, record created, outcomes exclusive, record persists, dynamical Born, rank-one Lüders (SwapMeasurementClosure).

• born_frequency {Ω : Type} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → UnifiedArena M) : (∀ (n : ℕ), Measurable (X n)) → (∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = arenaLiouville M p₀) → (∀ (i : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' (fun (a : UnifiedArena M) => a.1.1) ⁻¹' (SigmaLayer.productSector H hH p₀).pi ⁻¹' LF4.bornRegion ψ hψ0 i).indicator fun (x : Ω) => 1)) → ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' (fun (a : UnifiedArena M) => a.1.1) ⁻¹' (SigmaLayer.productSector H hH p₀).pi ⁻¹' LF4.bornRegion ψ hψ0 i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

  Born frequency: i.i.d. trials of the arena Liouville measure land in the arena cylinder of the Born region with frequency → ‖⟨eᵢ,ψ⟩‖².

• mixed_born (ρ : LF2.DensityOperator (M + 1)) (i : Fin (M + 1)) : ∑ j : Fin (M + 1), ⋯.eigenvalues j * ((arenaLiouville M p₀) ((fun (a : UnifiedArena M) => a.1.1) ⁻¹' (SigmaLayer.productSector H hH p₀).pi ⁻¹' LF4.bornRegion (⋯.eigenvectorBasis j) ⋯ i)).toReal = LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)

  Mixed states: spectral mixtures of arena cylinder measures reproduce Tr(ρEᵢ).

theorem CSD.RecordLayer.unifiedArenaClosure {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : UnifiedArenaClosure H hH p₀ ψ hψ0

★★ The unified-arena closure holds — for every Hermitian H, base point p₀, and unit state ψ: one arena, one Liouville measure family, the rank-one reconstruction.

The mixed two-stage LLN, on the arena (the first recorded residue, discharged)

noncomputable def CSD.RecordLayer.arenaMixtureMeasure {M : ℕ} (p₀ : LF4.CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) : MeasureTheory.Measure (Fin (M + 1) × UnifiedArena M)

The two-stage mixture measure on the arena: draw a spectral component, then an arena microstate from the arena Liouville measure.

Equations

• CSD.RecordLayer.arenaMixtureMeasure p₀ ρ = (CSD.SigmaLayer.eigenvalueMeasure ρ).prod (CSD.RecordLayer.arenaLiouville M p₀)

def CSD.RecordLayer.arenaMixtureRegion {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) (i : Fin (M + 1)) : Set (Fin (M + 1) × UnifiedArena M)

The mixed outcome-i region on the arena: the system-slot cylinder of the two-stage Born region.

Equations

• CSD.RecordLayer.arenaMixtureRegion H hH p₀ ρ i = (Prod.map id fun (a : CSD.RecordLayer.UnifiedArena M) => a.1.1) ⁻¹' CSD.SigmaLayer.mixtureRegion H hH p₀ ρ i

theorem CSD.RecordLayer.arena_mixed_born_frequency {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (Y : ℕ → Ω → Fin (M + 1) × UnifiedArena M) (hY : ∀ (n : ℕ), Measurable (Y n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (Y n) Pr = arenaMixtureMeasure p₀ ρ) (hindep : ∀ (i : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (Y n ⁻¹' arenaMixtureRegion H hH p₀ ρ i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (Y k ⁻¹' arenaMixtureRegion H hH p₀ ρ i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)))

Mixed-state Born frequencies, on the unified arena. For i.i.d. two-stage trials of any density operator ρ — spectral component, then arena microstate — the outcome-i frequency converges a.s. to Tr(ρ Eᵢ). Transfers from unified_mixed_born_frequency through the system-slot marginal; discharges the residue recorded at the migration.

The round trip (the second recorded residue, discharged)

theorem CSD.RecordLayer.readout_arenaIso {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (s : ℝ) (y : UnifiedArena M) : (swapProtocol (basinIndex (momentContext (M + 1))) ⋯).readout (arenaIso H hH p₀ s y) = (swapProtocol (basinIndex (momentContext (M + 1))) ⋯).readout y

Records are invariant under isolated evolution: the lifted exp(-itH) never touches the pointer register, so the readout is a conserved quantity of the isolated flow. This is what "the record is a stable fact of Σ" means dynamically.

theorem CSD.RecordLayer.arena_round_trip {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (r s : ℝ) (i : Fin (M + 1)) (x : UnifiedArena M) (hx : arenaIso H hH p₀ r x ∈ selReadyBank (basinIndex (momentContext (M + 1))) i) : (swapProtocol (basinIndex (momentContext (M + 1))) ⋯).readout (arenaIso H hH p₀ s ((swapProtocol (basinIndex (momentContext (M + 1))) ⋯).evolve 0 1 (arenaIso H hH p₀ r x))) = some i

★ The round trip: isolate, measure, isolate — the record is created and survives. Evolve freely for time r; if the evolved state sits in the selector-i ready set, run the measurement: the record i is created, and any subsequent isolated evolution for time s leaves it standing. The first statement in the corpus that composes the Schrödinger propagator and the measurement propagator on one arena — the composition that was not even stateable before the migration.