LF6-A.3: a manifestly LOCAL product de-isolation flow realising the singlet

Category: 6-Local (the entangled de-isolation tier; the D1 entangled frontier).

This is LF6-A.3 of specs/lf6-plan.md. It completes the LF6-A entangled-tier stage by exhibiting a manifestly local product de-isolation V_loc = V_A ⊗ V_B — each wing an LF5 single-system (N = 2) de-isolation — and proving it realises the SAME joint measurement as the A.2 flow: its context-fixed pointer-block Fubini–Study volumes are the LF3 singlet kernel P_st. So the de-isolation needs no non-local interaction; the non-locality is entirely in the contextual carve (LF6-A.2) and the entangled preparation (SO-1).

Honest framing (read this; do not get it wrong)

LF6-A.2's flow is measurementFlow 4 finProdFinEquiv, whose underlying unitary is the adder σ(j,k) = (j, j+k) on ℤ/4. That N = 4 adder unitary does NOT factor as (N=2 adder) ⊗ (N=2 adder), because ℤ/4 (cyclic) is not ℤ/2 × ℤ/2 (Klein four) — mod-4 addition has carries. So A.3 is not "prove the A.2 flow factors" (it does not, as a full unitary).

A.3 instead constructs a manifestly local product de-isolation V_loc := V_A ⊗ V_B (each V_w the LF5 vnDilationV at N = 2, the wing copy / CNOT in the local axis basis), reindexed onto the joint dilated space, and proves it realises the same joint measurement (same pointer-block volumes = P_st). The factorisation is then by construction (V_loc is defined as a tensor product, localDeisolation_factorises); the genuine new content is that this local product dilation is a Naimark dilation of the joint product POVM (localDeisolation_pullback, composing the two wing LF5 pullbacks via the Kronecker (A⊗B)ᴴ(P⊗Q)(A⊗B) = (AᴴPA)⊗(BᴴQB) identity) and so reproduces the singlet (localDeisolation_pointer_volume, routing through the LF4 POVM-Naimark volume engine + LF3 singletJointEig_born).

So: the N=4-adder A.2 flow is one (non-factoring) unitary completion of the joint measurement; A.3's product flow is the manifestly-local realisation, showing the de-isolation CAN be local.

The construction (clean path)

The local product dilation is a Naimark dilation of the joint computational-basis POVM, with the pullback factorising into per-wing pullbacks:

V_loc := V_A ⊗ V_B                                     -- V_w = LF5 vnDilationV @ N=2
(V_loc)ᴴ (Π^A_i ⊗ Π^B_j) (V_loc)
   = ((V_A)ᴴ Π^A_i V_A) ⊗ ((V_B)ᴴ Π^B_j V_B)          -- tensor of pullbacks
   = |a_i⟩⟨a_i| ⊗ |b_j⟩⟨b_j|                            -- each wing: vnDilationV_pullback @ N=2
   = |a_i ⊗ b_j⟩⟨a_i ⊗ b_j|                              -- joint rank-1 projector

Reindexing the genuine tensor product (rows (sys_A ⊗ ptr_A) ⊗ (sys_B ⊗ ptr_B), columns sys_A ⊗ sys_B) onto the Naimark form (system Fin 4, ancilla Fin 4) is the jointDilEquiv / jointSysEquiv regrouping ((s_a,p_a),(s_b,p_b)) ↦ ((s_a,s_b),(p_a,p_b)). The block reshuffle blockProj 4 i = reindex (blockProj 2 i_a ⊗ blockProj 2 i_b) (blockProj_localReindex) is the load-bearing transport lemma.

Honest scope (the A.3 ledger)

• Exhibited. A genuinely local product de-isolation V_loc = V_A ⊗ V_B (localDeisolationV, localDeisolation_factorises — V_loc is a tensor product), a Naimark dilation of the joint basis POVM (localDeisolation_pullback, the tensor-pullback composing the two wing LF5 pullbacks), whose pointer-block FS volumes reproduce the singlet kernel (localDeisolation_pointer_volume = P_st); the projectivised product flow is FS-measure-preserving and ≠ id (localDeisolationFlow_*).
• Imported, not re-derived. Born = FS-volume is derived one layer down (the moment-map / Duistermaat–Heckman cluster, Gleason-free, no Born put in) and imported via povm_born_eq_dilated_volume_uncond; the singlet kernel P_st, its joint eigenstates, and the Born identity singletJointEig_born are LF3.
• Residue: SO-1. The entangled sector / the singlet's preparation region is posited, not derived (SO-1: the sector origin, distinct from Paper C Axiom A5). The non-locality lives in the contextual carve (A.2) and the entangled preparation, never in the (local) flow.
• Generic context. hgen : ∀ s t, 0 < P_st a b s t (|a·b| < 1) — the generic non-collinear contexts, which include the four canonical CHSH-optimal pairs. ⚠️ Collinear settings are Bell-test settings too and are excluded here; LF6.localDeisolation_pointer_volume_local covers them.

All exports are foundational-triple-only (Gleason-free; the LF4/LF5 POVM-Naimark volume engine is off Busch).

Reference: specs/lf6-plan.md (LF6-A.3).

Boolean-indicator algebra helper

theorem CSD.LF6.ite_mul_ite_one {P Q : Prop} [Decidable P] [Decidable Q] : ((if P then 1 else 0) * if Q then 1 else 0) = if P ∧ Q then 1 else 0

Product of two 0/1 indicators is the indicator of the conjunction.

The reindexing equivs (the system / dilated-space regrouping)

def CSD.LF6.jointSysEquiv : Fin 2 × Fin 2 ≃ Fin 4

The joint system reindex sys_A ⊗ sys_B ≃ Fin 4.

Equations

• CSD.LF6.jointSysEquiv = finProdFinEquiv

def CSD.LF6.jointDilEquiv : (Fin 2 × Fin 2) × Fin 2 × Fin 2 ≃ Fin 4 × Fin 4

The joint dilated-space regrouping (sys_A ⊗ ptr_A) ⊗ (sys_B ⊗ ptr_B) ≃ Fin 4 × Fin 4, sending ((s_a,p_a),(s_b,p_b)) to ((s_a,s_b), (p_a,p_b)) (system block, ancilla block) and reindexing each sys/ptr pair by jointSysEquiv. This is the regrouping that turns the product tensor V_A ⊗ V_B into the Naimark form V : Fin 4 × Fin 4 ← Fin 4.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CSD.LF6.jointDilEquiv_symm_apply (s a : Fin 4) : jointDilEquiv.symm (s, a) = (((jointSysEquiv.symm s).1, (jointSysEquiv.symm a).1), (jointSysEquiv.symm s).2, (jointSysEquiv.symm a).2)

theorem CSD.LF6.single_submatrix_symm {β : Type u_1} {γ : Type u_2} [Fintype β] [DecidableEq β] [Fintype γ] [DecidableEq γ] (e : β ≃ γ) (p : β) : (Matrix.single p p 1).submatrix ⇑e.symm ⇑e.symm = Matrix.single (e p) (e p) 1

A diagonal computational-basis projector transports through an equiv reindex as a relabelling of its index: (|e_p⟩⟨e_p|).submatrix e.symm e.symm = |e_{e p}⟩⟨e_{e p}|.

Deliverable 1: the per-wing de-isolation

noncomputable def CSD.LF6.wingDeisolationV : Matrix (Fin 2 × Fin 2) (Fin 2) ℂ

The per-wing N = 2 de-isolation unitary V_w = U_vN ∘ (· ⊗ a₀) (the LF5 vnDilationV at N = 2: the wing copy / CNOT in the local axis basis). Its column space is the single wing system ℂ²; its dilated space is sys ⊗ ptr.

Equations

• CSD.LF6.wingDeisolationV = CSD.LF5.vnDilationV 2

theorem CSD.LF6.wingDeisolation_pullback (i : Fin 2) : wingDeisolationV.conjTranspose * LF4.blockProj 2 i * wingDeisolationV = ((LF5.basisPOVM 2).E i).M

The wing Naimark pullback (V_w)ᴴ Π^w_i V_w = |a_i⟩⟨a_i| — the LF5 vnDilationV_pullback at N = 2.

Deliverable 3 (the genuine new content): the tensor pullback

theorem CSD.LF6.localDeisolation_pullback (i j : Fin 2) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) wingDeisolationV wingDeisolationV).conjTranspose * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF4.blockProj 2 i) (LF4.blockProj 2 j) * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) wingDeisolationV wingDeisolationV = Matrix.single (i, j) (i, j) 1

The local product dilation is a Naimark dilation of the joint product POVM (the tensor-pullback lemma, LF6-A.3 crux). (V_A ⊗ V_B)ᴴ (Π^A_i ⊗ Π^B_j) (V_A ⊗ V_B) = |a_i ⊗ b_j⟩⟨a_i ⊗ b_j|.

The proof genuinely composes the two wing LF5 pullbacks: push the conjugate transpose across the Kronecker (conjTranspose_kronecker), fold the two Kronecker products into one (← mul_kronecker_mul twice) to expose (V_wᴴ Π^w V_w) ⊗ (V_wᴴ Π^w V_w), discharge each factor by wingDeisolation_pullback (= |e_i⟩⟨e_i|), and recombine the matrix-unit Kronecker |e_i⟩⟨e_i| ⊗ |e_j⟩⟨e_j| = |e_{(i,j)}⟩⟨e_{(i,j)}| (single_kronecker_single).

Reading the projector (do not mistake the computational for the physical). The proved RHS |e_{(i,j)}⟩⟨e_{(i,j)}| is the computational-basis rank-1 projector. It reads the physical wing outcomes (a_i at wing A, b_j at wing B) because the preparation carries the axis context, not because the frame is rotated: the prepared state in localDeisolation_pointer_volume is nudgedSinglet a b, not the bare singlet, and its coordinates are the setting-dependent moduli √(P_st a b s t) (each the overlap ⟨ψ⁻, singletJointEig s t a b⟩). So the computational weight at cell (s, t) is the (a, b)-context outcome probability by nudgedSinglet_born, and no basis rotation is invoked.

⚠️ Do not read this as a rotated frame (corrected 2026-08-19; erratum E-2, specs/publication-errata.md). This paragraph previously said the axis context was "carried by the nudgedSinglet a b rotation" and that these were "the physical eigenprojectors expressed in the rotated frame". That is false for the same reason the definition site records: nudgedSinglet discards every relative phase, and at a ⊥ b it is ½(1,1,1,1), a product state, while ψ⁻ is maximally entangled — so no local unitary relates them off a·b = ±1. The genuinely local-unitary object with the same Born statistics is LF6.localNudgeVec; cite that if a rotated-frame reading is wanted. Nothing here is affected, because this proof consumes only ‖·‖².

Deliverable 2: the local product dilation and its factorisation

noncomputable def CSD.LF6.localDeisolationV : Matrix (Fin 4 × Fin 4) (Fin 4) ℂ

The local product de-isolation isometry V_loc = V_A ⊗ V_B, reindexed onto the Naimark form Fin 4 × Fin 4 ← Fin 4. It is, by construction, the Kronecker product of the two identical wing de-isolations.

Equations

• CSD.LF6.localDeisolationV = (Matrix.reindex CSD.LF6.jointDilEquiv CSD.LF6.jointSysEquiv) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) CSD.LF6.wingDeisolationV CSD.LF6.wingDeisolationV)

theorem CSD.LF6.localDeisolation_factorises : (Matrix.reindex jointDilEquiv jointSysEquiv).symm localDeisolationV = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) wingDeisolationV wingDeisolationV

The de-isolation IS a tensor product (the locality, by construction). Stripping the dilated-space / system reindexings recovers exactly the Kronecker product of the two wing de-isolations: V_loc factorises as V_A ⊗ V_B. This is the manifest-locality content of A.3.

theorem CSD.LF6.localDeisolation_isom : localDeisolationV.conjTranspose * localDeisolationV = 1

V_loc is an isometry (V_loc)ᴴ V_loc = 1: the Kronecker of two isometries is an isometry (vnDilationV_isom per wing + one_kronecker_one), transported through the reindex (submatrix_mul_equiv + submatrix_one_equiv).

theorem CSD.LF6.blockProj_localReindex (i j : Fin 2) : LF4.blockProj 4 (jointSysEquiv (i, j)) = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF4.blockProj 2 i) (LF4.blockProj 2 j)).submatrix ⇑jointDilEquiv.symm ⇑jointDilEquiv.symm

The block reshuffle (load-bearing transport lemma). The Naimark ancilla-i projector blockProj 4 (jointSysEquiv (i,j)) on Fin 4 × Fin 4 equals the reindexed product of the two wing block projectors blockProj 2 i ⊗ blockProj 2 j on (sys_A⊗ptr_A)⊗(sys_B⊗ptr_B) — the ((s_a,p_a),(s_b,p_b)) ↦ ((s_a,s_b),(p_a,p_b)) regrouping made matrix-level.

theorem CSD.LF6.localDeisolation_naimark_pullback (i' : Fin 4) : localDeisolationV.conjTranspose * LF4.blockProj 4 i' * localDeisolationV = ((LF5.basisPOVM 4).E i').M

The Naimark pullback for the local product dilation (in the Naimark Fin 4 × Fin 4 form): (V_loc)ᴴ Π_i V_loc = |e_i⟩⟨e_i| = ((basisPOVM 4).E i).M. Transports the tensor pullback localDeisolation_pullback through the reshuffle blockProj_localReindex and the reindex (submatrix_mul_equiv, single_submatrix_symm).

noncomputable def CSD.LF6.localNaimark : LF4.NaimarkDilation (LF5.basisPOVM 4)

The local product dilation as a Naimark dilation of the joint computational-basis POVM basisPOVM 4. The dilation isometry is the manifestly local V_loc = V_A ⊗ V_B.

Equations

• CSD.LF6.localNaimark = { V := CSD.LF6.localDeisolationV, isom := CSD.LF6.localDeisolation_isom, pullback := CSD.LF6.localDeisolation_naimark_pullback }

theorem CSD.LF6.localDeisolation_norm_map (ψ : EuclideanSpace ℂ (Fin 4)) : ‖(Matrix.toEuclideanLin localDeisolationV) ψ‖ = ‖ψ‖

Operator-level isometry: ‖V_loc ψ‖ = ‖ψ‖.

Deliverable 4: the local product flow reproduces the singlet

theorem CSD.LF6.localDeisolation_pointer_volume {M : ℕ} (a b : LF3.DetectorSetting) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st a b s t) (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin localDeisolationV) (nudgedSinglet a b))) (hψ'0 : ψ' ≠ 0) (s t : LF3.Sign) : ∑ n : Fin 4, ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (n, stIdx (s, t))))).toReal = LF3.P_st a b s t

The reproduction (the A.3 headline). The LOCAL product de-isolation V_loc = V_A ⊗ V_B reproduces the singlet: its context-fixed pointer-block (s, t) Fubini–Study volume equals the LF3 singlet kernel P_st a b s t, for the prepared state φ = nudgedSinglet a b (the setting-dependent moduli √(P_st a b s t), reused from A.2 — not a locally rotated singlet; see the erratum note on localDeisolation_pullback above and LF6.localNudgeVec for the object that genuinely is a local-unitary image).

The proof routes the local product Naimark dilation localNaimark through the LF4 POVM-Naimark volume machinery povm_born_eq_dilated_volume_uncond (Born = FS-volume imported from the DH/FS-volume engine, Gleason-free) and reads the POVM weight via basisPOVM_weight + the LF3 Born identity behind nudgedSinglet_born (singletJointEig_born). So a manifestly LOCAL flow gives the same pointer-block volumes as the (non-factoring) N=4-adder A.2 flow.

Deliverable 5: the projectivised local product flow

theorem CSD.LF6.vnUnitaryKron_mem : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF5.vnUnitary 2) (LF5.vnUnitary 2) ∈ Matrix.unitaryGroup ((Fin 2 × Fin 2) × Fin 2 × Fin 2) ℂ

The product wing-coupling unitary U_A ⊗ U_B is a unitary: the Kronecker of two unitaries (vnUnitary_unitary per wing + one_kronecker_one).

def CSD.LF6.jointFlowEquiv : (Fin 2 × Fin 2) × Fin 2 × Fin 2 ≃ Fin (4 * 4)

The reindex equiv carrying the product dilated space onto Fin (4*4).

Equations

• CSD.LF6.jointFlowEquiv = CSD.LF6.jointDilEquiv.trans finProdFinEquiv

noncomputable def CSD.LF6.localFlowUnitary : ↥(Matrix.unitaryGroup (Fin (4 * 4)) ℂ)

The local product flow unitary U_loc = U_A ⊗ U_B, reindexed onto Fin 16: a manifestly local product unitary on the dilated projective space.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.LF6.vnUnitaryKron_mulVec_single (z1 z2 : Fin 2 × Fin 2) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF5.vnUnitary 2) (LF5.vnUnitary 2)).mulVec (Pi.single (z1, z2) 1) = Pi.single ((LF5.vnPerm 2) z1, (LF5.vnPerm 2) z2) 1

Basis action of the product unitary U_A ⊗ U_B: it permutes the computational basis by vnPerm 2 on each wing.

theorem CSD.LF6.localFlowUnitary_toEuclideanLin_single (z1 z2 : Fin 2 × Fin 2) : (Matrix.toEuclideanLin ↑localFlowUnitary) (EuclideanSpace.single (jointFlowEquiv (z1, z2)) 1) = EuclideanSpace.single (jointFlowEquiv ((LF5.vnPerm 2) z1, (LF5.vnPerm 2) z2)) 1

The flow unitary's Euclidean basis action.

noncomputable def CSD.LF6.localDeisolationFlow : Projectivization ℂ (EuclideanSpace ℂ (Fin (4 * 4))) → Projectivization ℂ (EuclideanSpace ℂ (Fin (4 * 4)))

The local product de-isolation flow Φ_loc = (U_loc • ·) on the dilated projective ontic space ℂℙ¹⁵ = ℙ(EuclideanSpace ℂ (Fin 16)). Manifestly local (U_loc = U_A ⊗ U_B).

Equations

• CSD.LF6.localDeisolationFlow p = CSD.LF6.localFlowUnitary • p

theorem CSD.LF6.localDeisolationFlow_measurePreserving (p₀ : LF4.CPN (4 * 4)) : MeasureTheory.MeasurePreserving localDeisolationFlow (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The local product flow is Fubini–Study measure-preserving (the Liouville / hΦ_pres content) — directly from fubiniStudyMeasure_smul_invariant for the product unitary U_loc.

theorem CSD.LF6.localDeisolationFlow_mk_single (z1 z2 : Fin 2 × Fin 2) : localDeisolationFlow (Projectivization.mk ℂ (EuclideanSpace.single (jointFlowEquiv (z1, z2)) 1) ⋯) = Projectivization.mk ℂ (EuclideanSpace.single (jointFlowEquiv ((LF5.vnPerm 2) z1, (LF5.vnPerm 2) z2)) 1) ⋯

Basis-ray action of the local product flow: it moves the ray at jointFlowEquiv (z1, z2) to the one at jointFlowEquiv (vnPerm 2 z1, vnPerm 2 z2).

theorem CSD.LF6.localDeisolationFlow_ne_id : localDeisolationFlow ≠ id

The local product flow is genuinely not the identity (Φ_loc ≠ id): the basis ray at jointFlowEquiv ((1,0),(1,0)) (both wings: system 1, ground apparatus) moves to the distinct ray at jointFlowEquiv ((1,1),(1,1)) — the product coupling correlates each apparatus with its system.

Deliverable 6 (the flow ↔ dilation tie): the local flow realises the dilation

This section closes the auditor Minor on LF6-A.3: the capstone previously bundled the local flow Φ_loc (localDeisolationFlow) and the local Naimark dilation V_loc (localDeisolationV) without a theorem tying them. Here we prove the LF5 measurementFlow_realises_dilation analogue: at the projective level, the LOCAL product flow carries the embedded ray [ψ ⊗ (a₀ ⊗ a₀)] exactly to the dilated ray [V_loc ψ]. The tie is genuine and routine: V_loc = U_loc ∘ (· ⊗ ground) because each wing is vnDilationV 2 = vnUnitary 2 * embedGround 2, so the product dilation factors through the product flow U_loc = U_A ⊗ U_B.

noncomputable def CSD.LF6.localEmbedGround : Matrix (Fin 4 × Fin 4) (Fin 4) ℂ

The local product ground-state embedding ψ ↦ ψ ⊗ (a₀ ⊗ a₀), reindexed onto the dilated space Fin 4 × Fin 4 ← Fin 4 exactly as localDeisolationV. It is the Kronecker product of the two identical wing ground embeddings embedGround 2, so localDeisolationV = U_loc ∘ embed (localDeisolationV_eq).

Equations

• CSD.LF6.localEmbedGround = (Matrix.reindex CSD.LF6.jointDilEquiv CSD.LF6.jointSysEquiv) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CSD.LF5.embedGround 2) (CSD.LF5.embedGround 2))

theorem CSD.LF6.localEmbedGround_isom : localEmbedGround.conjTranspose * localEmbedGround = 1

The ground embedding is an isometry embedᴴ embed = 1: the Kronecker of two embedGround 2 isometries (embedGround_isom per wing + one_kronecker_one), transported through the reindex. Mirrors localDeisolation_isom.

noncomputable def CSD.LF6.localFlowReindexed : Matrix (Fin 4 × Fin 4) (Fin 4 × Fin 4) ℂ

The local product flow unitary as a matrix on Fin 4 × Fin 4 (the dilated space before the final finProdFinEquiv reindex onto Fin 16). It is the Kronecker U_A ⊗ U_B reindexed by jointDilEquiv; reindex finProdFinEquiv · recovers localFlowUnitary.val (localFlowReindexed_reindex).

Equations

• CSD.LF6.localFlowReindexed = (Matrix.reindex CSD.LF6.jointDilEquiv CSD.LF6.jointDilEquiv) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CSD.LF5.vnUnitary 2) (CSD.LF5.vnUnitary 2))

theorem CSD.LF6.localDeisolationV_eq : localDeisolationV = localFlowReindexed * localEmbedGround

The dilation factors through the flow (matrix level): V_loc = U_loc ∘ embed. Genuine content: each wing vnDilationV 2 is vnUnitary 2 * embedGround 2, so the Kronecker V_A ⊗ V_B splits as (U_A ⊗ U_B) * (embed_A ⊗ embed_B) (mul_kronecker_mul); the shared dilated middle index is folded by submatrix_mul_equiv.

theorem CSD.LF6.localFlowReindexed_reindex : (Matrix.reindex finProdFinEquiv finProdFinEquiv) localFlowReindexed = ↑localFlowUnitary

The flow-matrix reindex coherence: pushing localFlowReindexed along the final finProdFinEquiv recovers the flow unitary localFlowUnitary.val. Both are (vnUnitary 2 ⊗ₖ vnUnitary 2) submatrixed; the index functions agree because jointFlowEquiv = jointDilEquiv.trans finProdFinEquiv.

theorem CSD.LF6.toEuclideanLin_localEmbedGround_ne_zero (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ψ ≠ 0) : (Matrix.toEuclideanLin localEmbedGround) ψ ≠ 0

The embedded vector of a nonzero preparation is nonzero (embed is isometric).

theorem CSD.LF6.toEuclideanLin_localDeisolationV_ne_zero (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ψ ≠ 0) : (Matrix.toEuclideanLin localDeisolationV) ψ ≠ 0

The post-flow vector of a nonzero preparation is nonzero (V_loc is isometric).

theorem CSD.LF6.localEmbed_ne_zero (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ψ ≠ 0) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv) ((Matrix.toEuclideanLin localEmbedGround) ψ) ≠ 0

The reindexed embedded ray representative is nonzero (piLpCongrLeft isometry).

theorem CSD.LF6.localDil_ne_zero (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ψ ≠ 0) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv) ((Matrix.toEuclideanLin localDeisolationV) ψ) ≠ 0

The reindexed post-flow ray representative is nonzero.

theorem CSD.LF6.localDeisolationFlow_realises_operator (ψ : EuclideanSpace ℂ (Fin 4)) : (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv) ((Matrix.toEuclideanLin localDeisolationV) ψ) = (Matrix.toEuclideanLin ↑localFlowUnitary) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv) ((Matrix.toEuclideanLin localEmbedGround) ψ))

The flow ↔ dilation operator identity: V_loc ψ (reindexed onto Fin 16) equals the flow unitary U_loc applied to the embedded vector ψ ⊗ (a₀ ⊗ a₀) (reindexed). Composes the matrix factorisation localDeisolationV_eq (V_loc = U_loc ∘ embed), the toEuclideanLin-of-product split, the reindex naturality toEuclideanLin_reindex_piLpCongrLeft, and the flow-reindex coherence localFlowReindexed_reindex.

theorem CSD.LF6.localDeisolationFlow_realises_localNaimark (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ψ ≠ 0) : localDeisolationFlow (Projectivization.mk ℂ ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv) ((Matrix.toEuclideanLin localEmbedGround) ψ)) ⋯) = Projectivization.mk ℂ ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv) ((Matrix.toEuclideanLin localDeisolationV) ψ)) ⋯

The LOCAL flow realises the local Naimark dilation (the A.3 flow ↔ dilation tie). At the projective level, the local product de-isolation flow Φ_loc carries the embedded ray [ψ ⊗ (a₀ ⊗ a₀)] exactly to the dilated ray [V_loc ψ], for every nonzero preparation ψ : EuclideanSpace ℂ (Fin 4). So the local Naimark dilation localNaimark consumed by the volume engine is dynamically realised by the manifestly local flow — a theorem of the dynamics, matching LF5's measurementFlow_realises_dilation. Proof: smul_mk_eq_mk + mk_eq_mk_iff' discharged by the operator identity localDeisolationFlow_realises_operator.

Deliverable 7: the capstone

theorem CSD.LF6.localDeisolation_capstone {M : ℕ} (a b : LF3.DetectorSetting) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st a b s t) (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin localDeisolationV) (nudgedSinglet a b))) (hψ'0 : ψ' ≠ 0) (q₀ : LF4.CPN (4 * 4)) : (Matrix.reindex jointDilEquiv jointSysEquiv).symm localDeisolationV = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) wingDeisolationV wingDeisolationV ∧ (∀ (i j : Fin 2), (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) wingDeisolationV wingDeisolationV).conjTranspose * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF4.blockProj 2 i) (LF4.blockProj 2 j) * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) wingDeisolationV wingDeisolationV = Matrix.single (i, j) (i, j) 1) ∧ (∀ (s t : LF3.Sign), ∑ n : Fin 4, ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (n, stIdx (s, t))))).toReal = LF3.P_st a b s t) ∧ MeasureTheory.MeasurePreserving localDeisolationFlow (Matrix.UnitaryGroup.fubiniStudyMeasure q₀) (Matrix.UnitaryGroup.fubiniStudyMeasure q₀) ∧ localDeisolationFlow ≠ id ∧ ∀ (φ : EuclideanSpace ℂ (Fin 4)) (hφ : φ ≠ 0), localDeisolationFlow (Projectivization.mk ℂ ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv) ((Matrix.toEuclideanLin localEmbedGround) φ)) ⋯) = Projectivization.mk ℂ ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv) ((Matrix.toEuclideanLin localDeisolationV) φ)) ⋯

The LF6-A.3 capstone: a manifestly LOCAL product de-isolation realises the singlet. Conjuncts:

1. the de-isolation IS a tensor product V_loc = V_A ⊗ V_B (localDeisolation_factorises) — manifest locality, by construction;
2. it is a Naimark dilation of the joint product POVM: the tensor pullback (V_A⊗V_B)ᴴ (Π^A_i ⊗ Π^B_j) (V_A⊗V_B) = |a_i⊗b_j⟩⟨a_i⊗b_j| (localDeisolation_pullback), composing the two wing LF5 pullbacks;
3. the LOCAL product flow reproduces the singlet: pointer-block FS volume = P_st for every (s,t) sector (localDeisolation_pointer_volume). ⚠️ Generic contexts only — this conjunct carries hgen, so it says nothing at a·b = ±1. The hgen-free version is LF6.localDeisolation_pointer_volume_local (NudgeLocality.lean), which covers every setting pair including the perfectly (anti)correlated ones;
4. the projectivised product flow is FS-measure-preserving (localDeisolationFlow_measurePreserving);
5. and genuinely ≠ id (localDeisolationFlow_ne_id);
6. the LOCAL flow realises the local Naimark dilation: Φ_loc [ψ ⊗ (a₀ ⊗ a₀)] = [V_loc ψ] for every nonzero preparation (localDeisolationFlow_realises_localNaimark) — the flow ↔ dilation tie, so the dilation whose carve gives P_st (conjunct 3) is dynamically realised by the manifestly local flow, matching LF5's measurement_flow_realises_dilation.

So the de-isolation apparatus coupling needs no non-local interaction. The N=4-adder A.2 flow is a non-factoring unitary completion of the same measurement (ℤ/4 ≠ ℤ/2 × ℤ/2); A.3's product flow is the manifestly-local one. Born = FS-volume is imported (LF5/DH/POVM-Naimark engine), not re-derived.

⚠️ Three distinct things, which must not be run together (sharpened 2026-08-10):

1. The local context-setting operation. LOCAL, but only via LF6.localNudge — not via nudgedSinglet, which strips every phase and is a product state at a ⊥ b, hence no local-unitary image of the singlet.
2. The local de-isolation apparatus coupling. LOCAL, and proved here (localDeisolation_factorises). Composed with (1), the whole finite chain factorises: LF6.localMeasurementChain_factorises.
3. Bell factorisation of outcomes. IMPOSSIBLE for the singlet (no_product_partition_realises_singlet), and nothing above weakens that.

(1) and (2) are dynamical locality of the finite dilated construction; they are not a canonical subsystem decomposition of an arbitrary ontic Σ, and none is used or implied.

Residue: SO-1 (the entangled sector posited, never derived). Honest ledger: module docstring.