SigmaLayer/PovmDynamics: POVM and instrument dynamics via Naimark dilation

Category: dynamical measurement — the POVM/instrument tier of the record layer.

A POVM is not a new kind of measurement: it is a projective measurement on a dilated space, watched through an isometry. This module makes that dictum dynamical. Given a POVM P on ℂ^N with outcomes Fin K and any Naimark dilation V : ℂ^N → ℂ^N ⊗ ℂ^K (LF4.canonicalNaimark supplies one for every POVM), prepare the dilated ray [Vψ] on the flat index and run the existing degenerate record protocol with the ancilla block structure localBlock N K — no new dynamics, no new sectors, no new arena:

• ★ povm_selector_born — the block selector's outcome-i fibre at the dilated preparation carries exactly ⟨ψ, Eᵢ ψ⟩: the POVM Born rule at the selector level. ⚠️ Corrected 2026-08-04 (codebase audit). — this said "the dynamical POVM Born rule", which overstates it. The statement is an epistemicMeasure of a selector fibre blockIndex ⁻¹' {i}, i.e. degenerate_selector_born transported along the dilation; no protocol, propagator or outcome sector appears in its type. The corpus draws exactly this distinction in SwapClosure.lean ("sector_born is the dynamical Born, not the kinematic selector Born"), and join_sector_born (JoinClosure.lean) shows what the protocol-level form costs (preimage_sector_ae + volume_goodTheta). Lifting this to the sector form is a recorded extension — delivered 2026-08-04: SigmaLayer/PovmSectorBorn.lean, povm_sector_born. The selector-level statement below remains as the kinematic ingredient it always was.
• ★ toComposite_blockProj_dilate — the record-layer block projection of the dilated preparation IS the ancilla projection Πᵢ(Vψ) under the index transport: the post-measurement rays the join witness delivers are the Naimark–Lüders instrument post-states.
• ★★ povm_instrument — the join witness's post-measurement system marginals satisfy the degenerate-Lüders demand at the dilated preparation: outcome i relocates the dilated system to [Πᵢ(Vψ)].
• ★★ naimarkInstrumentClosure / naimarkInstrumentClosureCanonical — the bundle (statistics + instrument + Naimark identification), for every dilation, and via the canonical dilation for every POVM.

⚠️ Honest scope. (i) The outcome set is Fin K — what the record protocol's outcome space speaks; an arbitrary Fintype index is a transport away and not restated. (ii) The instrument delivered is the Lüders instrument of the dilation. A POVM does not determine its instrument (that is physics, not a defect — distinct dilations give distinct, equally legitimate state updates with the same statistics); what is proved is that this dilation's instrument is dynamically realised. (iii) The dilated preparation [Vψ] is the entry point: the isometry represents the pre-measurement coupling of the system to a ready ancilla (the standard factorisation V = U(· ⊗ |0⟩)); realising V itself as a unitary-plus-ancilla stroke inside the record dynamics is a recorded extension, not claimed here. (iv) Mixed preparations compose exactly as in SigmaLayer/MixedSwap.lean (two-stage sampling) and are not restated on the dilated space.

References

specs/BACKLOG.md (the POVM/instrument-dynamics row — this discharges it); specs/future-work.md; LF2/POVM.lean (POVM, POVM.weight); LF4/POVMDilation.lean (NaimarkDilation, LF4.blockProj, born_transfer), LF4/POVMNaimark.lean (canonicalNaimark); SigmaLayer/DegenerateLuders.lean (blockIndex, degenerate_selector_born, BlockLudersObligation), SigmaLayer/JoinLuders.lean (joinPostMarg, joinWitness_blockLuders), SigmaLayer/LocalBlockBridge.lean (localBlock, toComposite, toComposite_blockProj), SigmaLayer/MeasurementCapstone.lean (the projective layer this rides on).

instance CSD.RecordLayer.instNeZeroNatHMul_csdLean4 {N K : ℕ} [NeZero N] [NeZero K] : NeZero (N * K)

The dilated dimension is positive.

The dilated preparation

noncomputable def CSD.RecordLayer.dilate {N K : ℕ} {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) : EuclideanSpace ℂ (Fin N × Fin K)

The dilated preparation on the composite index: the isometric image Vψ of the system preparation under the Naimark dilation.

Equations

• CSD.RecordLayer.dilate D ψ = (Matrix.toEuclideanLin D.V) ψ

noncomputable def CSD.RecordLayer.dilateFlat {N K : ℕ} {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) : EuclideanSpace ℂ (Fin (N * K))

The dilated preparation on the flat index Fin (N·K) — the index the record protocol's arena speaks — obtained by pulling back along finProdFinEquiv.

Equations

• CSD.RecordLayer.dilateFlat D ψ = WithLp.toLp 2 fun (j : Fin (N * K)) => (CSD.RecordLayer.dilate D ψ).ofLp (finProdFinEquiv.symm j)

@[simp]

theorem CSD.RecordLayer.dilateFlat_apply {N K : ℕ} {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) (j : Fin (N * K)) : (dilateFlat D ψ).ofLp j = (dilate D ψ).ofLp (finProdFinEquiv.symm j)

theorem CSD.RecordLayer.toComposite_dilateFlat {N K : ℕ} {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) : toComposite (dilateFlat D ψ) = dilate D ψ

The index transport recovers the composite form of the dilated preparation.

theorem CSD.RecordLayer.norm_dilate {N K : ℕ} {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) : ‖dilate D ψ‖ = ‖ψ‖

The dilation is isometric on preparations: ‖Vψ‖ = ‖ψ‖, from Vᴴ V = 1.

theorem CSD.RecordLayer.norm_dilateFlat {N K : ℕ} {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) : ‖dilateFlat D ψ‖ = ‖ψ‖

theorem CSD.RecordLayer.dilateFlat_ne_zero {N K : ℕ} {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) : dilateFlat D ψ ≠ 0

The block Born weights of the dilated preparation are the POVM weights

theorem CSD.RecordLayer.sum_block_normSq_dilate {N K : ℕ} (P : LF2.POVM N (Fin K)) (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin K) : ∑ j : Fin (N * K) with localBlock N K j = i, ‖inner ℂ (EuclideanSpace.single j 1) (dilateFlat D ψ)‖ ^ 2 = P.weight ψ i

The spectral bridge for POVMs: the fine-grained Born weights of the dilated preparation, summed over the ancilla block of outcome i, are exactly the POVM Born weight ⟨ψ, Eᵢ ψ⟩. Left side: the sum degenerate_selector_born produces. Right side: born_transfer reads it off the dilated inner product against Πᵢ.

★ The POVM Born rule, at the selector level

theorem CSD.RecordLayer.povm_selector_born {N K : ℕ} [NeZero N] [NeZero K] (P : LF2.POVM N (Fin K)) (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin K) : (epistemicMeasure (Projectivization.mk ℂ (dilateFlat D ψ) ⋯)) (blockIndex (localBlock N K) ⁻¹' {i}) = ENNReal.ofReal (P.weight ψ i)

★ The POVM Born rule at the selector level. (Prose corrected 2026-08-04: this was called "the dynamical POVM Born rule"; the statement is the measure of a selector fibre, not of a protocol outcome sector — see the module docstring.) Prepare the dilated ray [Vψ] and run the degenerate record protocol with the ancilla block structure localBlock N K: the outcome-i sector carries exactly the POVM Born weight ⟨ψ, Eᵢ ψ⟩. Statistics of an arbitrary POVM, realised by the existing projective record dynamics on the dilated arena.

★ The post-states are the Naimark–Lüders instrument

theorem CSD.RecordLayer.toComposite_blockProj_dilate {N K : ℕ} {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin K) : toComposite ((blockProj (localBlock N K) i) (dilateFlat D ψ)) = (Matrix.toEuclideanLin (LF4.blockProj N i)) (dilate D ψ)

★ The record-layer block posts are the Naimark–Lüders posts. The block projection of the dilated preparation, transported back to the composite index, IS the ancilla projection Πᵢ(Vψ) — so the post-measurement rays the join witness delivers on the dilated arena are exactly the instrument post-states of the dilation.

theorem CSD.RecordLayer.povm_instrument {N K : ℕ} [NeZero N] [NeZero K] {P : LF2.POVM N (Fin K)} (D : LF4.NaimarkDilation P) (α : Fin K → EuclideanSpace ℂ (Fin (N * K))) (hα : ∀ (i : Fin K), (blockProj (localBlock N K) i) (α i) = α i) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) (h : (blockProj (localBlock N K) i) (dilateFlat D ψ) ≠ 0) : joinPostMarg (localBlock N K) α (dilateFlat D ψ) ⋯ i = epistemicMeasure (Projectivization.mk ℂ ((blockProj (localBlock N K) i) (dilateFlat D ψ)) h)

★★ POVM instrument dynamics. At the dilated preparation, the join witness's post-measurement system marginals satisfy the degenerate-Lüders demand: conditioning on outcome i relocates the dilated system to the epistemic state of [Πᵢ(Vψ)] — by toComposite_blockProj_dilate, the Naimark–Lüders instrument post-state. Delivered by joinWitness_blockLuders, i.e. by Liouville-preserving dynamics on the join arena, not by fiat.

★★ The closure

structure CSD.RecordLayer.NaimarkInstrumentClosure {N K : ℕ} [NeZero N] [NeZero K] (P : LF2.POVM N (Fin K)) (D : LF4.NaimarkDilation P) : Prop

What the POVM/instrument tier delivers, bundled — for a POVM P and a Naimark dilation D: the selector-level POVM Born rule at every unit preparation, the inhabited degenerate-Lüders obligation on the dilated arena (the instrument), and the identification of the block posts with the Naimark–Lüders posts Πᵢ(Vψ).

• born (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : ‖ψ‖ = 1 → ∀ (i : Fin K), (epistemicMeasure (Projectivization.mk ℂ (dilateFlat D ψ) ⋯)) (blockIndex (localBlock N K) ⁻¹' {i}) = ENNReal.ofReal (P.weight ψ i)

  The POVM Born rule at the selector level.

• instrument (α : Fin K → EuclideanSpace ℂ (Fin (N * K))) : (∀ (i : Fin K), (blockProj (localBlock N K) i) (α i) = α i) → BlockLudersObligation (localBlock N K) (joinPostMarg (localBlock N K) α)

  The instrument: block-Lüders on the dilated arena, inhabited by the join witness.

• naimark_posts (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin K) : toComposite ((blockProj (localBlock N K) i) (dilateFlat D ψ)) = (Matrix.toEuclideanLin (LF4.blockProj N i)) (dilate D ψ)

  The block posts are the Naimark–Lüders posts.

theorem CSD.RecordLayer.naimarkInstrumentClosure {N K : ℕ} [NeZero N] [NeZero K] (P : LF2.POVM N (Fin K)) (D : LF4.NaimarkDilation P) : NaimarkInstrumentClosure P D

★★ The POVM/instrument closure, for every dilation.

theorem CSD.RecordLayer.naimarkInstrumentClosureCanonical {N K : ℕ} [NeZero N] [NeZero K] (P : LF2.POVM N (Fin K)) : NaimarkInstrumentClosure P (LF4.canonicalNaimark P)

★★ Every POVM has dynamically realised statistics and instrument, via its canonical Naimark dilation (LF4.canonicalNaimark, the CFC square-root construction).