LF5: de-isolation realises the Naimark dilation (LF5-C)

Category: 3-Local (LF5 measurement-dynamics layer).

This is LF5-C of specs/lf5-plan.md: the dilation isometry of the canonical projective (computational-basis) measurement, dynamically realised by the von Neumann coupling. The static, unmotivated Naimark embedding V of the LF4 POVM tranche is here exhibited as

  V  =  U_vN ∘ (· ⊗ a₀)        (vnDilationV = vnUnitary * embedGround)

— embed the system in the apparatus ground state a₀ = e₀, then evolve by the LF5-A von Neumann coupling unitary. The post-flow vector is the correlated state U_vN (ψ ⊗ a₀) = ∑ⱼ ψⱼ · (eⱼ ⊗ aⱼ) (vnDilationV_mulVec), the pointer-outcome regions are the context-fixed apparatus blocks blockProj N i (the apparatus basis, not carved to Born), and the headline vnNaimark inhabits NaimarkDilation (basisPOVM N):

• vnDilationV_isom — Vᴴ V = 1 (the de-isolation embedding is isometric);
• vnDilationV_pullback — Vᴴ (blockProj N i) V = |eᵢ⟩⟨eᵢ| (the crux: the context-fixed pointer block compresses to the projective effect);
• measurementFlow_realises_dilation — at the projective level, the LF5-B flow Φ_vN carries the embedded ray [ψ ⊗ a₀] exactly to the dilated ray [Vψ], so the dilation is a theorem of the dynamics, not a gloss.

Honest scope

Single-system projective tier (basisPOVM, the rank-1 computational-basis measurement). The Born = FS-volume identity is derived one layer down (the moment-map / Duistermaat–Heckman cluster, fs_born_volume_ratio_N, Gleason-free) and downstream (LF5-D) imported, not re-proved and not postulated; this module supplies the dynamical origin of the dilation isometry that engine consumes. What is posited is not Born but the CSD sector (SO-1) — the Fubini–Study measure as the dilated sector's typicality law (a theorem that Born = volume; a posit that FS is the typicality measure, reducing to D1). Entangled / non-local de-isolation is deferred (specs/lf5-plan.md §0).

LF5-D obstruction (recorded at planning; RESOLVED)

The post-flow state Vψ has zero amplitude on every off-diagonal cell (j, k) with k ≠ j (vnDilationV_mulVec). Hence the genericity hypothesis hpos of povm_born_eq_dilated_volume / povm_born_frequency_volume (all N·N dilated amplitudes nonzero) is not satisfiable at ψ' = piLpCongrLeft e (Vψ) for N ≥ 2 (at N = 1 there is no off-diagonal cell). LF5-D therefore could not be a blind instantiation of the P.3b/P.4 theorems: it needed either a zero-amplitude-tolerant volume reading on the dilated space or a system-side reduction. vnDilation_block_weight (block-i weight of the post-flow state = the Born weight ‖⟨eᵢ, ψ⟩‖²) is the Gleason-free analytic content already available on this side of that gap.

Resolution (historical record kept above): the FS-volume engine was upgraded hpos-free (LF4/BornRegionUncond.lean, povm_born_eq_dilated_volume_uncond / povm_born_frequency_volume_uncond, per-cell dichotomy); LF5-D (FlowBornFrequency.lean) consumes the unconditional forms, and the corpus-wide call-site migration onto them landed 2026-06-11.

Reference: specs/lf5-plan.md (LF5-C).

The computational-basis projective POVM

theorem CSD.LF5.outerProduct_single {N : ℕ} (i : Fin N) : LF2.outerProduct (EuclideanSpace.single i 1) = Matrix.single i i 1

Rank-1 outer product of a basis vector is a matrix unit: |eᵢ⟩⟨eᵢ| = single i i 1. Entries: (eᵢ)_a · star (eᵢ)_b = δ_{a i} δ_{b i}.

noncomputable def CSD.LF5.basisPOVM (N : ℕ) : LF2.POVM N (Fin N)

The computational-basis projective POVM Eᵢ = |eᵢ⟩⟨eᵢ|: the canonical rank-1 projective measurement the von Neumann coupling reads out. Completeness is ∑ᵢ |eᵢ⟩⟨eᵢ| = ∑ᵢ single i i 1 = 1.

Equations

• CSD.LF5.basisPOVM N = { E := fun (i : Fin N) => CSD.LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯, complete := ⋯ }

theorem CSD.LF5.basisPOVM_E_M {N : ℕ} (i : Fin N) : ((basisPOVM N).E i).M = Matrix.single i i 1

The effect matrix of the basis POVM is the matrix unit single i i 1.

theorem CSD.LF5.single_one_mulVec_apply {N : ℕ} (i a : Fin N) (v : Fin N → ℂ) : (Matrix.single i i 1).mulVec v a = if i = a then v i else 0

Action of the matrix unit single i i 1 on a vector: (single i i 1 *ᵥ v) a = δ_{i a} · v i.

theorem CSD.LF5.basisPOVM_weight {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin N) : (basisPOVM N).weight ψ i = ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2

Rank-1 Born weight of the basis POVM. The i-th weight of preparation ψ is the Born quadratic form ‖⟨eᵢ, ψ⟩‖².

theorem CSD.LF5.basisPOVM_weight_coord {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin N) : (basisPOVM N).weight ψ i = ‖ψ.ofLp i‖ ^ 2

Coordinate form of the basis-POVM Born weight: pᵢ(ψ) = ‖ψᵢ‖².

Isometry helper

theorem CSD.LF5.toEuclideanLin_norm_map_of_isom {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {A : Matrix κ ι ℂ} (hA : A.conjTranspose * A = 1) (ψ : EuclideanSpace ℂ ι) : ‖(Matrix.toEuclideanLin A) ψ‖ = ‖ψ‖

A matrix with Aᴴ A = 1 induces a norm-preserving map on EuclideanSpace: ‖Aψ‖² = re⟨Aψ, Aψ⟩ = re⟨ψ, Aᴴ A ψ⟩ = ‖ψ‖² via the matrix↔operator adjoint bridge. Generic helper (Mathlib upstream candidate).

The ground-state embedding ψ ↦ ψ ⊗ a₀

def CSD.LF5.embedGround (N : ℕ) [NeZero N] : Matrix (Fin N × Fin N) (Fin N) ℂ

The ground-state embedding matrix of ψ ↦ ψ ⊗ a₀ (apparatus ground a₀ = e₀): (embedGround N)_{(j,k), m} = δ_{(j,k), (m,0)}.

Equations

• CSD.LF5.embedGround N = Matrix.of fun (p : Fin N × Fin N) (m : Fin N) => if p = (m, 0) then 1 else 0

theorem CSD.LF5.embedGround_apply {N : ℕ} [NeZero N] (p : Fin N × Fin N) (m : Fin N) : embedGround N p m = if p = (m, 0) then 1 else 0

theorem CSD.LF5.embedGround_column {N : ℕ} [NeZero N] (m : Fin N) : (fun (p : Fin N × Fin N) => embedGround N p m) = Pi.single (m, 0) 1

Column m of the ground embedding is the dilated basis vector e_{(m,0)} (system m, apparatus ground).

theorem CSD.LF5.embedGround_mulVec {N : ℕ} [NeZero N] (v : Fin N → ℂ) (j k : Fin N) : (embedGround N).mulVec v (j, k) = if k = 0 then v j else 0

The embedded vector in coordinates: (ψ ⊗ a₀)_{(j,k)} = δ_{k,0} · ψⱼ.

theorem CSD.LF5.embedGround_isom {N : ℕ} [NeZero N] : (embedGround N).conjTranspose * embedGround N = 1

The ground embedding is an isometry: embedᴴ embed = 1 (the columns e_{(m,0)} are orthonormal).

theorem CSD.LF5.embedGround_norm_map {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin (embedGround N)) ψ‖ = ‖ψ‖

Operator-level isometry of the ground embedding: ‖ψ ⊗ a₀‖ = ‖ψ‖.

The dynamically-realised dilation isometry V = U_vN ∘ (· ⊗ a₀)

noncomputable def CSD.LF5.vnDilationV (N : ℕ) [NeZero N] : Matrix (Fin N × Fin N) (Fin N) ℂ

The dynamically-realised Naimark dilation isometry V = U_vN ∘ (· ⊗ a₀): embed the system in the apparatus ground state, then evolve by the LF5-A von Neumann coupling. This replaces the unmotivated static Naimark embedding of the LF4 POVM tranche with the de-isolation dynamics.

Equations

• CSD.LF5.vnDilationV N = CSD.LF5.vnUnitary N * CSD.LF5.embedGround N

theorem CSD.LF5.vnDilationV_column {N : ℕ} [NeZero N] (m : Fin N) : (fun (p : Fin N × Fin N) => vnDilationV N p m) = Pi.single (m, m) 1

Column m of V is the correlated basis vector e_{(m,m)}: the coupling sends e_m ⊗ a₀ to e_m ⊗ a_m (vnUnitary_mulVec_ground).

theorem CSD.LF5.vnDilationV_apply {N : ℕ} [NeZero N] (p : Fin N × Fin N) (m : Fin N) : vnDilationV N p m = if p = (m, m) then 1 else 0

Entry formula: V_{p, m} = δ_{p, (m,m)}.

theorem CSD.LF5.vnDilationV_mulVec_eq {N : ℕ} [NeZero N] (v : Fin N → ℂ) : (vnDilationV N).mulVec v = (vnUnitary N).mulVec ((embedGround N).mulVec v)

The dynamical reading of V, explicit: V ψ = U_vN (ψ ⊗ a₀) at the mulVec level.

theorem CSD.LF5.vnDilationV_mulVec {N : ℕ} [NeZero N] (v : Fin N → ℂ) (j k : Fin N) : (vnDilationV N).mulVec v (j, k) = if k = j then v j else 0

The post-flow vector in coordinates: U_vN (ψ ⊗ a₀) = ∑ⱼ ψⱼ · (eⱼ ⊗ aⱼ), i.e. (Vψ)_{(j,k)} = δ_{k j} · ψⱼ. The system and the apparatus pointer are perfectly correlated; every off-diagonal cell (j, k), k ≠ j, carries zero amplitude (the LF5-D hpos obstruction recorded in the module docstring).

theorem CSD.LF5.vnDilationV_isom {N : ℕ} [NeZero N] : (vnDilationV N).conjTranspose * vnDilationV N = 1

V is an isometry: Vᴴ V = embedᴴ (U_vNᴴ U_vN) embed = embedᴴ embed = 1 (unitarity of the coupling + isometry of the ground embedding).

theorem CSD.LF5.vnDilationV_norm_map {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin (vnDilationV N)) ψ‖ = ‖ψ‖

Operator-level isometry: ‖Vψ‖ = ‖ψ‖ (feeds LF5-D's hnorm).

theorem CSD.LF5.blockProj_mul_vnDilationV {N : ℕ} [NeZero N] (i n j m : Fin N) : (LF4.blockProj N i * vnDilationV N) (n, j) m = if j = i ∧ n = m ∧ i = m then 1 else 0

The pointer-i block projector acting on V: (Πᵢ V)_{(n,j), m} = δ_{j i} δ_{n m} δ_{m i} — only the (i, i) cell of column i survives.

theorem CSD.LF5.vnDilationV_pullback {N : ℕ} [NeZero N] (i : Fin N) : (vnDilationV N).conjTranspose * LF4.blockProj N i * vnDilationV N = ((basisPOVM N).E i).M

The Naimark pullback, dynamically realised (the LF5-C crux): the context-fixed pointer block compresses through the de-isolation isometry to the projective effect, Vᴴ (blockProj N i) V = |eᵢ⟩⟨eᵢ|.

noncomputable def CSD.LF5.vnNaimark (N : ℕ) [NeZero N] : LF4.NaimarkDilation (basisPOVM N)

The LF5-C headline: the canonical projective measurement's Naimark dilation, dynamically realised by the von Neumann coupling. The dilation isometry is V = U_vN ∘ (· ⊗ a₀) — measurement-flow dynamics, not a static embedding — and the pointer regions are the context-fixed apparatus blocks.

Equations

• CSD.LF5.vnNaimark N = { V := CSD.LF5.vnDilationV N, isom := ⋯, pullback := ⋯ }

theorem CSD.LF5.vnDilation_block_weight {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin N) : RCLike.re (inner ℂ ((Matrix.toEuclideanLin (vnDilationV N)) ψ) ((Matrix.toEuclideanLin (LF4.blockProj N i)) ((Matrix.toEuclideanLin (vnDilationV N)) ψ))) = ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2

Block-i weight of the post-flow state = the Born weight. The dilated projective Born weight of Vψ = U_vN (ψ ⊗ a₀) against the context-fixed pointer block Πᵢ is ‖⟨eᵢ, ψ⟩‖². Composes the Naimark Born transfer with the rank-1 basis-POVM weight; Gleason-free.

The LF5-B flow realises the dilation at the projective level

theorem CSD.LF5.toEuclideanLin_vnDilationV {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) : (Matrix.toEuclideanLin (vnDilationV N)) ψ = (Matrix.toEuclideanLin (vnUnitary N)) ((Matrix.toEuclideanLin (embedGround N)) ψ)

Operator form of the factorisation V = U_vN ∘ (· ⊗ a₀).

theorem CSD.LF5.toEuclideanLin_reindex_piLpCongrLeft {N m : ℕ} (e : Fin N × Fin N ≃ Fin m) (A : Matrix (Fin N × Fin N) (Fin N × Fin N) ℂ) (w : EuclideanSpace ℂ (Fin N × Fin N)) : (Matrix.toEuclideanLin ((Matrix.reindex e e) A)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) w) = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin A) w)

Reindex naturality: transporting a matrix along e and a vector along the piLpCongrLeft e isometry commutes with toEuclideanLin. Reduces to Matrix.submatrix_mulVec_equiv at the function level.

theorem CSD.LF5.piLpCongrLeft_vnDilationV {N : ℕ} [NeZero N] {m : ℕ} (e : Fin N × Fin N ≃ Fin m) (ψ : EuclideanSpace ℂ (Fin N)) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV N)) ψ) = (Matrix.toEuclideanLin ↑(vnUnitaryReindexed N e)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (embedGround N)) ψ))

The reindexed post-flow vector is the reindexed coupling applied to the reindexed embedded vector: the vector-level identity behind measurementFlow_realises_dilation.

theorem CSD.LF5.toEuclideanLin_embedGround_ne_zero {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) : (Matrix.toEuclideanLin (embedGround N)) ψ ≠ 0

The embedded vector of a nonzero preparation is nonzero.

theorem CSD.LF5.toEuclideanLin_vnDilationV_ne_zero {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) : (Matrix.toEuclideanLin (vnDilationV N)) ψ ≠ 0

The post-flow vector of a nonzero preparation is nonzero.

theorem CSD.LF5.piLpCongrLeft_embedGround_ne_zero {N : ℕ} [NeZero N] {m : ℕ} (e : Fin N × Fin N ≃ Fin m) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (embedGround N)) ψ) ≠ 0

The reindexed embedded vector is nonzero (piLpCongrLeft is an isometry).

theorem CSD.LF5.piLpCongrLeft_vnDilationV_ne_zero {N : ℕ} [NeZero N] {m : ℕ} (e : Fin N × Fin N ≃ Fin m) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV N)) ψ) ≠ 0

The reindexed post-flow vector is nonzero.

theorem CSD.LF5.measurementFlow_realises_dilation {N : ℕ} [NeZero N] {m : ℕ} (e : Fin N × Fin N ≃ Fin m) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) : measurementFlow N e (Projectivization.mk ℂ ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (embedGround N)) ψ)) ⋯) = Projectivization.mk ℂ ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV N)) ψ)) ⋯

The flow ↔ dilation tie: at the projective level, the LF5-B measurement flow Φ_vN carries the embedded ray [ψ ⊗ a₀] exactly to the dilated ray [Vψ]. The Naimark dilation consumed by the LF4 POVM volume engine is therefore dynamically realised by the de-isolation flow — a theorem tying the flow to the dilation, not a gloss. (The mathematical crux of the tranche is vnDilationV_pullback; this theorem's content is the reindex naturality plus the definitional factorisation V = U_vN · embed.)