LF6-D: the general d x d maximally-entangled de-isolation flow

Category: 6-Local (the first genuinely DIMENSION-GENERAL instance of CSD's D1 entangled frontier; the general-d analogue of the singlet's LF6-A.2 and the GHZ's LF6-C.2).

Before this file the entangled de-isolation tier had exactly two hand-built instances: the 2x2 singlet (LF6-A) and the three-qubit GHZ (LF6-C). This module makes "general-N" actually general: it instantiates the LF5 general-N de-isolation engine at N = d * d for the bipartite maximally-entangled state Ψ_d = (1/√d) ∑_i |i⟩|i⟩ on EuclideanSpace ℂ (Fin d × Fin d), for every d ≥ 2, and lands the pointer-block Fubini-Study volumes on the maximally-mixed Born weights 1/d, with a.s. block frequencies converging to them.

The construction (reusing LF5 @ N = d·d)

The bipartite system ℂ^{d²} ≅ ℂ^d ⊗ ℂ^d is measured by the LF5 von Neumann de-isolation flow measurementFlow (d*d) e on the dilated projective ontic space Σ' = ℂℙ^{d²·d²−1}. The flow is inherited wholesale from LF5-B at N = d*d; it is genuinely Φ ≠ id (1 < d*d, i.e. d ≥ 2) and Fubini-Study measure-preserving. The prepared state is Ψ_d reindexed to the computational Fin (d*d) basis (nudgedMaxEntangled d). Then the headline:

pointer-block w FS volume  =  ‖⟨e_{medIdx w}, nudgedMaxEntangled d⟩‖²   -- LF5 @ N=d·d
                           =  ‖(maxEntangled d) w‖²                       -- reindex identity
                           =  medWeight d w                               -- 1/d on the diagonal, 0 off

So the reproduction is LF5@N=d·d + a coordinate (reindex-isometry) step + the computed maximally-entangled Born weights medWeight.

Honest scope (the D ledger)

• Dimension-general, exhibited. A genuine deterministic FS-measure-preserving de-isolation flow Φ ≠ id for every d ≥ 2 (maxEntangledDeisolation_*), whose context-fixed BornRegion pointer-block volumes equal the Born weights medWeight (maxEntangledDeisolation_pointer_volume) and whose a.s. block frequencies converge to them (maxEntangledDeisolation_frequency). This is the load-bearing content: the LF6 de-isolation dynamics + Born-from-volume is now GENUINELY DIMENSION-GENERAL, not tied to 2x2 / GHZ.
• Imported, not re-derived. Born = FS-volume is the DH/moment-map cluster's (fs_born_volume_ratio_N, Gleason-free, no Born put in), imported through vnDilation_pointer_volume; this file does not re-derive it. What is exercised is the measurement dynamics (Φ ≠ id).
• Realisation, not derivation. The flow realises the measurement dynamically; it does not derive the weights from independent dynamics. The carve is the joint moment subdivision, never a setting-local product region.
• Forced non-factorisation, derived and maxEntangled-specific. Ψ_d's {0,1}×{0,1} Schmidt sector is derived (full state, coherences included) to be the Bell Φ⁺ state up to the positive scalar √2/√d (maxEntangledSector_eq_phiPlus). Φ⁺'s two-qubit Pauli correlation is computed here from the Hilbert space (phiPlus_pauli_correlation: ⟨Φ⁺|σ·a ⊗ σ·b|Φ⁺⟩ = a_x b_x − a_y b_y + a_z b_z), and no product (setting-local, non-contextual) partition reproduces it (no_product_partition_realises_phiPlus). The CHSH violation is genuinely Φ⁺'s: the orthogonal xz-reflection of Bob's axis (reflectXZ) carries E_{Φ⁺} to the singlet's −a·b (phiPlusCorrelation_reflectXZ), so Φ⁺ reaches the same 2√2 > 2, contradicting the LHV cap |S| ≤ 2 (lhvCHSH_abs_le_two). So no_product_partition_realises_maxEntangled is Bell-forced and maxEntangled-specific (the Φ⁺ correlation is derived and identified with the sector, not the singlet's −a·b imported by prose). Scope: non-factorisation forced by the CHSH-violating 2x2 Φ⁺ sector. This is now superseded for every d ≥ 2 by the genuinely d-intrinsic CGLMP violation of Ψ_d (CGLMPQudit.no_lhv_realises_maxEntangled_cglmp_d, CGLMPQudit.cglmp_maxEntangled_qudit_gt_two: cglmp d pQM > 2 for all d ≥ 2, computed from Ψ_d's actual Born probabilities via the Dirichlet-kernel closed form), with d = 3 (cglmp 3 pQM = (12+8√3)/9) the concrete qutrit anchor. The general-d CGLMP result is now closed.
• Residue: SO-1. The entangled sector / preparation region is posited, not derived (SO-1: the sector origin, distinct from Paper C Axiom A5); the typicality law on Σ' is the Fubini-Study measure (SO-1).

All exports are foundational-triple-only (Gleason-free; the LF5 pointer engine is off Busch, A.1 is measure-theoretic Bell content).

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

instance CSD.LF6.neZero_mul_self (d : ℕ) [NeZero d] : NeZero (d * d)

d * d is nonzero whenever d is (targeted local instance so the LF5 engine at N = d * d synthesises [NeZero (d * d)] from [NeZero d]).

The maximally-entangled Born weights

noncomputable def CSD.LF6.medWeight (d : ℕ) (w : Fin d × Fin d) : ℝ

The maximally-entangled Born weights. Ψ_d = (1/√d) ∑_i |i⟩|i⟩ has support exactly on the diagonal {(i, i)}, each computational cell carrying weight 1/d; every off-diagonal cell has weight 0. This is the maximally-mixed (Schmidt-rank-d) weight vector. Not a stub: maxEntangled_normSq_eq_weight proves it equals ‖(maxEntangled d) w‖².

Equations

• CSD.LF6.medWeight d w = if w.1 = w.2 then (↑d)⁻¹ else 0

The maximally-entangled state

noncomputable def CSD.LF6.maxEntangled (d : ℕ) : EuclideanSpace ℂ (Fin d × Fin d)

The bipartite maximally-entangled state Ψ_d = (1/√d) ∑_i |i⟩|i⟩ on EuclideanSpace ℂ (Fin d × Fin d): the computational amplitude is (√d)⁻¹ on the diagonal and 0 off it. Schmidt rank d; unit-norm for d ≥ 1.

Equations

• CSD.LF6.maxEntangled d = WithLp.toLp 2 fun (w : Fin d × Fin d) => if w.1 = w.2 then (↑√↑d)⁻¹ else 0

theorem CSD.LF6.maxEntangled_apply (d : ℕ) (w : Fin d × Fin d) : (maxEntangled d).ofLp w = if w.1 = w.2 then (↑√↑d)⁻¹ else 0

The computational amplitude of Ψ_d at cell w.

theorem CSD.LF6.maxEntangled_normSq_eq_weight (d : ℕ) (w : Fin d × Fin d) : ‖(maxEntangled d).ofLp w‖ ^ 2 = medWeight d w

The Born weights are the squared computational amplitudes. For every computational cell w, ‖(maxEntangled d) w‖² = medWeight d w — genuinely computed from the diagonal amplitude (√d)⁻¹ (‖·‖² = 1/d) and the off-diagonal zeros.

theorem CSD.LF6.sum_medWeight (d : ℕ) (hd : 0 < d) : ∑ w : Fin d × Fin d, medWeight d w = 1

The maximally-entangled Born weights sum to 1 (the d diagonal cells, each 1/d; the off-diagonal cells 0). The prepared state is normalised.

The diagonal Born-weight marginal is uniform (1/d)

theorem CSD.LF6.maxEntangled_marginal_uniform (d : ℕ) (i : Fin d) : ∑ j : Fin d, medWeight d (i, j) = (↑d)⁻¹

The diagonal Born-weight marginal is uniform (1/d). For every system index i, the marginal Born weight ∑_j medWeight d (i, j) = 1/d (one diagonal cell contributes 1/d, the rest 0). This is the diagonal (computational-basis Born-weight) marginal only; it is the maximal-entanglement signature at that level (a uniform diagonal marginal is necessary for ρ_A = I/d), but it does NOT by itself establish ρ_A = I/d (the off-diagonal vanishing of the reduced state is a separate fact, not proved here). Holds for every d ≥ 1 (the sole i diagonal cell contributes 1/d).

The CHSH-violating 2x2 maximally-entangled sector

def CSD.LF6.sectorEmbed (d : ℕ) (hd : 2 ≤ d) : Fin 2 → Fin d

The Schmidt-block embedding Fin 2 ↪ Fin d (indices 0, 1), available for d ≥ 2. Picks out two Schmidt vectors per side.

Equations

• CSD.LF6.sectorEmbed d hd i = ⟨↑i, ⋯⟩

theorem CSD.LF6.sectorEmbed_injective (d : ℕ) (hd : 2 ≤ d) : Function.Injective (sectorEmbed d hd)

theorem CSD.LF6.medWeight_sector (d : ℕ) (hd : 2 ≤ d) (i j : Fin 2) : medWeight d (sectorEmbed d hd i, sectorEmbed d hd j) = if i = j then (↑d)⁻¹ else 0

The 2x2 sector Born weight in closed form. On the {0,1}×{0,1} Schmidt block the Born weight is 1/d on the diagonal (the two Schmidt vectors are the Φ⁺ support) and 0 off it — the embedding is injective, so sectorEmbed i = sectorEmbed j ↔ i = j.

theorem CSD.LF6.maxEntangled_sector_diagonal (d : ℕ) (hd : 2 ≤ d) (i : Fin 2) : medWeight d (sectorEmbed d hd i, sectorEmbed d hd i) = (↑d)⁻¹

The 2x2 sector diagonal weight. On the {0,1}×{0,1} Schmidt block the diagonal Born weight is 1/d (the two Schmidt vectors (0,0), (1,1) are the Φ⁺ support).

theorem CSD.LF6.maxEntangled_sector_offdiagonal (d : ℕ) (hd : 2 ≤ d) (i j : Fin 2) (hij : i ≠ j) : medWeight d (sectorEmbed d hd i, sectorEmbed d hd j) = 0

The 2x2 sector off-diagonal weight. Off the diagonal the sector Born weight is 0; the embedding is injective, so distinct sector indices map to distinct system indices.

theorem CSD.LF6.maxEntangled_sector_marginal_uniform (d : ℕ) (hd : 2 ≤ d) (i : Fin 2) : ∑ j : Fin 2, medWeight d (sectorEmbed d hd i, sectorEmbed d hd j) = (↑d)⁻¹

The 2x2 sector diagonal Born-weight marginal is uniform (1/d). The sector diagonal marginal ∑_j medWeight d (sectorEmbed i, sectorEmbed j) = 1/d is uniform over the two Schmidt vectors. This is the diagonal Born-weight signature that the {0,1}×{0,1} block is (up to the d-factor) the two-qubit maximally-entangled Bell state Φ⁺; the full state-level identification of the sector with Φ⁺ (coherences included) is maxEntangledSector_eq_phiPlus, and the sector's CHSH violation is no_product_partition_realises_phiPlus.

The Bell Φ⁺ state and the derived sector correlation

The genuine content that makes the non-factorisation maxEntangled-specific (not a verbatim re-export of the singlet no-go): the {0,1}×{0,1} Schmidt sector of Ψ_d is derived to be the Bell state Φ⁺ = (|00⟩+|11⟩)/√2 (maxEntangledSector_eq_phiPlus), whose two-qubit Pauli correlation ⟨Φ⁺|σ·a ⊗ σ·b|Φ⁺⟩ = a_x b_x − a_y b_y + a_z b_z is computed here from the Hilbert space (phiPlus_pauli_correlation), and whose CHSH violation forces non-factorisation (no_product_partition_realises_phiPlus).

noncomputable def CSD.LF6.phiPlus : EuclideanSpace ℂ (Fin 2 × Fin 2)

The Bell Φ⁺ state Φ⁺ = (1/√2)(|00⟩ + |11⟩) on EuclideanSpace ℂ (Fin 2 × Fin 2), unit-norm, the maximally-entangled symmetric Bell state. This is the two-qubit sector of Ψ_d.

Equations

• CSD.LF6.phiPlus = (↑√2)⁻¹ • (EuclideanSpace.single (0, 0) 1 + EuclideanSpace.single (1, 1) 1)

theorem CSD.LF6.phiPlus_apply_00 : phiPlus.ofLp (0, 0) = (↑√2)⁻¹

theorem CSD.LF6.phiPlus_apply_01 : phiPlus.ofLp (0, 1) = 0

theorem CSD.LF6.phiPlus_apply_10 : phiPlus.ofLp (1, 0) = 0

theorem CSD.LF6.phiPlus_apply_11 : phiPlus.ofLp (1, 1) = (↑√2)⁻¹

theorem CSD.LF6.phiPlus_apply_sector (i j : Fin 2) : phiPlus.ofLp (i, j) = if i = j then (↑√2)⁻¹ else 0

Φ⁺ amplitude in if i = j form on the Fin 2 × Fin 2 sector: (√2)⁻¹ on the diagonal (the (0,0), (1,1) support), 0 off it.

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

Expectation ⟨Φ⁺ | M | Φ⁺⟩ for a (Fin 2 × Fin 2)-indexed matrix M.

Equations

• CSD.LF6.phiPlusExpectation M = inner ℂ CSD.LF6.phiPlus ((Matrix.toEuclideanLin M) CSD.LF6.phiPlus)

theorem CSD.LF6.phiPlus_expectation_formula (M : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : phiPlusExpectation M = 1 / 2 * (M (0, 0) (0, 0) + M (0, 0) (1, 1) + M (1, 1) (0, 0) + M (1, 1) (1, 1))

Φ⁺ expectation formula. On the Bell Φ⁺ state the expectation of an arbitrary (Fin 2 × Fin 2)-indexed matrix reduces to a half-sum over the four diagonal-support entries. The 12 of 16 double-sum terms vanish (each has a Φ⁺(0,1) = 0 or Φ⁺(1,0) = 0 factor); the surviving 4 factor through ((√2)⁻¹)² = 1/2. Mirrors LF3.expectation_formula for Φ⁺'s (0,0)/(1,1) support.

noncomputable def CSD.LF6.phiPlusCorrelation (a b : LF3.DetectorSetting) : ℝ

The Φ⁺ correlation function in closed form, E_{Φ⁺}(a, b) = a_x b_x − a_y b_y + a_z b_z. Φ⁺ correlates σ_x/σ_z and anti-correlates σ_y; this is the derived Pauli expectation (phiPlus_pauli_correlation).

Equations

• CSD.LF6.phiPlusCorrelation a b = a.vec.ofLp 0 * b.vec.ofLp 0 - a.vec.ofLp 1 * b.vec.ofLp 1 + a.vec.ofLp 2 * b.vec.ofLp 2

theorem CSD.LF6.phiPlus_pauli_correlation (a b : LF3.DetectorSetting) : phiPlusExpectation (LF3.sigmaDotJoint a b) = ↑(phiPlusCorrelation a b)

The derived Φ⁺ two-qubit Pauli correlation (the load-bearing genuine computation): ⟨Φ⁺ | σ·a ⊗ σ·b | Φ⁺⟩ = a_x b_x − a_y b_y + a_z b_z, computed from the Hilbert space via phiPlus_expectation_formula and the pauliDot entries. This is Φ⁺'s own correlation, DERIVED — not the singlet's −a·b imported.

The 2x2 Schmidt sector is the Bell Φ⁺ state (derived)

noncomputable def CSD.LF6.maxEntangledSector (d : ℕ) (hd : 2 ≤ d) : EuclideanSpace ℂ (Fin 2 × Fin 2)

The {0,1}×{0,1} Schmidt sector of Ψ_d as a two-qubit vector: the restriction of maxEntangled d to the sector-embedded indices.

Equations

• CSD.LF6.maxEntangledSector d hd = WithLp.toLp 2 fun (w : Fin 2 × Fin 2) => (CSD.LF6.maxEntangled d).ofLp (CSD.LF6.sectorEmbed d hd w.1, CSD.LF6.sectorEmbed d hd w.2)

theorem CSD.LF6.maxEntangled_sector_apply (d : ℕ) (hd : 2 ≤ d) (i j : Fin 2) : (maxEntangled d).ofLp (sectorEmbed d hd i, sectorEmbed d hd j) = if i = j then (↑√↑d)⁻¹ else 0

Sector amplitude in if i = j form: (√d)⁻¹ on the diagonal, 0 off it (via the injectivity of sectorEmbed).

theorem CSD.LF6.maxEntangledSector_eq_phiPlus (d : ℕ) (hd : 2 ≤ d) : maxEntangledSector d hd = ↑(√2 / √↑d) • phiPlus

The 2x2 Schmidt sector IS the Bell Φ⁺ state (up to the positive real scalar √2/√d): maxEntangledSector d = (√2/√d) • Φ⁺. This is the derived, d-dependent, full-state (coherences included) identification of Ψ_d's {0,1}×{0,1} sector with the maximally-entangled Φ⁺ — the honest link making the sector's Φ⁺ correlation genuinely Ψ_d's sector correlation, for every d ≥ 2.

The reindexed (nudged) maximally-entangled state

def CSD.LF6.medIdx (d : ℕ) : Fin d × Fin d ≃ Fin (d * d)

The pointer-index identification (i, j) ↦ Fin (d*d) tying the LF5 pointer outcome at N = d*d to the bipartite computational basis.

Equations

• CSD.LF6.medIdx d = finProdFinEquiv

noncomputable def CSD.LF6.nudgedMaxEntangled (d : ℕ) : EuclideanSpace ℂ (Fin (d * d))

The prepared state. Ψ_d reindexed to the computational Fin (d*d) basis, nudgedMaxEntangled d k = (maxEntangled d) (medIdx d |>.symm k). For the minimal computational-basis carve the "nudge" is the identity context; the name mirrors A.2's nudgedSinglet / C.2's nudgedGHZ.

Equations

• CSD.LF6.nudgedMaxEntangled d = WithLp.toLp 2 fun (k : Fin (d * d)) => (CSD.LF6.maxEntangled d).ofLp ((CSD.LF6.medIdx d).symm k)

theorem CSD.LF6.nudgedMaxEntangled_coord (d : ℕ) (w : Fin d × Fin d) : (nudgedMaxEntangled d).ofLp ((medIdx d) w) = (maxEntangled d).ofLp w

The pointer-cell coordinate of the nudged state is the Ψ_d amplitude.

theorem CSD.LF6.nudgedMaxEntangled_born (d : ℕ) (w : Fin d × Fin d) : ‖inner ℂ (EuclideanSpace.single ((medIdx d) w) 1) (nudgedMaxEntangled d)‖ ^ 2 = medWeight d w

The nudge coordinate-Born identity. The squared computational amplitude of the nudged state at pointer cell w equals the Born weight medWeight d w — composing the reindex-coordinate identity with the computed weights.

theorem CSD.LF6.nudgedMaxEntangled_coord_normSq (d : ℕ) (w : Fin d × Fin d) : ‖(nudgedMaxEntangled d).ofLp ((medIdx d) w)‖ ^ 2 = medWeight d w

The pointer-cell squared coordinate as a function of the outcome pair.

theorem CSD.LF6.nudgedMaxEntangled_norm (d : ℕ) (hd : 0 < d) : ‖nudgedMaxEntangled d‖ = 1

The nudged state is a unit preparation. ‖φ‖² = ∑_w medWeight d w = 1. Discharges the hψ hypothesis of the LF5 pointer-volume / frequency theorems.

theorem CSD.LF6.nudgedMaxEntangled_ne_zero (d : ℕ) (hd : 0 < d) : nudgedMaxEntangled d ≠ 0

The nudged state is nonzero.

Deliverable 1: the flow

noncomputable def CSD.LF6.maxEntangledDeisolationFlow (d : ℕ) [NeZero d] : Projectivization ℂ (EuclideanSpace ℂ (Fin (d * d * (d * d)))) → Projectivization ℂ (EuclideanSpace ℂ (Fin (d * d * (d * d))))

The maximally-entangled de-isolation flow Φ = measurementFlow (d*d) finProdFinEquiv on the dilated projective ontic space Σ' = ℂℙ^{d²·d²−1}. This is the LF5-B von Neumann de-isolation flow instantiated at the bipartite system N = d*d.

Equations

• CSD.LF6.maxEntangledDeisolationFlow d = CSD.LF5.measurementFlow (d * d) finProdFinEquiv

theorem CSD.LF6.maxEntangledDeisolation_measurePreserving (d : ℕ) [NeZero d] (p₀ : LF4.CPN (d * d * (d * d))) : MeasureTheory.MeasurePreserving (maxEntangledDeisolationFlow d) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The maximally-entangled de-isolation flow is Fubini-Study measure-preserving (the Liouville / hΦ_pres content), inherited from measurementFlow_measurePreserving.

theorem CSD.LF6.maxEntangledDeisolation_ne_id (d : ℕ) [NeZero d] (hd : 2 ≤ d) : maxEntangledDeisolationFlow d ≠ id

The maximally-entangled de-isolation flow is genuinely not the identity for d ≥ 2 (1 < d*d), inherited from measurementFlow_ne_id.

Deliverable 2: pointer-block FS volume = Born weight (the headline)

theorem CSD.LF6.maxEntangledDeisolation_pointer_volume (d : ℕ) [NeZero d] {M : ℕ} (e : Fin (d * d) × Fin (d * d) ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (LF5.vnDilationV (d * d))) (nudgedMaxEntangled d))) (hψ'0 : ψ' ≠ 0) (w : Fin d × Fin d) : ∑ n : Fin (d * d), ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (n, (medIdx d) w)))).toReal = medWeight d w

The reproduction (the D headline). The context-fixed BornRegion pointer-block w Fubini-Study volume of the maximally-entangled de-isolation flow equals the Born weight medWeight d w, for the prepared state φ = nudgedMaxEntangled d, for every d ≥ 1.

The proof composes LF5 vnDilation_pointer_volume at N = d*d (pointer-block volume = ‖⟨e_i, φ⟩‖², Gleason-free, Born = FS-volume imported from the DH engine) with the nudge coordinate-Born identity nudgedMaxEntangled_born (the reindex-isometry step + the computed maximally-entangled weights). Dimension-general: the weights are the real maximally-mixed diagonal (1/d, …, 1/d).

Deliverable 3: a.s. pointer-block frequencies → Born weight

theorem CSD.LF6.maxEntangledDeisolation_frequency (d : ℕ) [NeZero d] {M : ℕ} (e : Fin (d * d) × Fin (d * d) ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (LF5.vnDilationV (d * d))) (nudgedMaxEntangled d))) (hψ'0 : ψ' ≠ 0) (p₀ : LF4.CPN (M + 1)) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN (M + 1)) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (w : Fin d × Fin d), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin (d * d), (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, (medIdx d) w))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (medWeight d w))

The empirical capstone. For i.i.d. Fubini-Study-typical trials on the dilated Σ' = ℂℙ^{d²·d²−1} (the sector-typicality posit (SO-1) on the enlarged entangled sector), almost surely every pointer-block w empirical frequency converges to the Born weight medWeight d w. Instantiates LF5 vnDilation_pointer_frequency at N = d*d, φ = nudgedMaxEntangled d, landing the limit on medWeight via nudgedMaxEntangled_born.

Deliverable 4: forced non-factorisation (Bell-forced via the derived Φ⁺ CHSH)

def CSD.LF6.reflectXZ (b : LF3.DetectorSetting) : LF3.DetectorSetting

The orthogonal xz-reflection on detector settings, reflectXZ (b_x, b_y, b_z) = (−b_x, b_y, −b_z). It is a norm-preserving involution mapping settings to settings; it carries the Φ⁺ correlation to the singlet's −a·b (phiPlusCorrelation_reflectXZ).

Equations

• CSD.LF6.reflectXZ b = { vec := !₂[-b.vec.ofLp 0, b.vec.ofLp 1, -b.vec.ofLp 2], unit := ⋯ }

@[simp]

theorem CSD.LF6.reflectXZ_vec_0 (b : LF3.DetectorSetting) : (reflectXZ b).vec.ofLp 0 = -b.vec.ofLp 0

@[simp]

theorem CSD.LF6.reflectXZ_vec_1 (b : LF3.DetectorSetting) : (reflectXZ b).vec.ofLp 1 = b.vec.ofLp 1

@[simp]

theorem CSD.LF6.reflectXZ_vec_2 (b : LF3.DetectorSetting) : (reflectXZ b).vec.ofLp 2 = -b.vec.ofLp 2

theorem CSD.LF6.phiPlusCorrelation_reflectXZ (a b : LF3.DetectorSetting) : phiPlusCorrelation a (reflectXZ b) = singletCorrelation a b

Φ⁺'s correlation = the singlet's under the xz-reflection of Bob's axis. E_{Φ⁺}(a, b) = −a·(reflectXZ b) = singletCorrelation a (reflectXZ b). This is the Φ⁺ ↔ ψ⁻ local-unitary transport at the correlation level (an orthogonal relabeling of Bob's setting), reducing Φ⁺'s CHSH to the singlet's.

LF6-7: the symmetric-sector Φ⁺ ↔ ψ⁻ transport recompute

The two Bell correlations were derived by two independent Hilbert-space computations — Φ⁺'s here in LF6-D (phiPlus_pauli_correlation) and ψ⁻'s separately in LF3 (LF3.singlet_pauli_correlation). Here the xz-reflection transport (phiPlusCorrelation_reflectXZ, so far only at the correlation-function level) is lifted to the HILBERT-SPACE expectation level: the singlet's −a·b is recomputed directly from Φ⁺'s own expectation, and the two independent derivations are proved to agree. This consolidates the antisymmetric (ψ⁻) sector as the reflectXZ-image of the symmetric (Φ⁺) sector — the Φ⁺ ↔ ψ⁻ transport recompute that was not yet done in LF6-D.

theorem CSD.LF6.phiPlus_pauli_correlation_reflectXZ (a b : LF3.DetectorSetting) : phiPlusExpectation (LF3.sigmaDotJoint a (reflectXZ b)) = ↑(singletCorrelation a b)

Transport recompute (Hilbert-space level). Feeding Bob's xz-reflected setting into Φ⁺'s derived Pauli expectation recomputes the singlet correlation: ⟨Φ⁺ | σ·a ⊗ σ·(reflectXZ b) | Φ⁺⟩ = singletCorrelation a b = −a·b. The ψ⁻ value is obtained as a corollary of the Φ⁺ computation via the local-unitary (xz-reflection) transport, not as a separate derivation.

theorem CSD.LF6.phiPlus_transport_eq_singlet_expectation (a b : LF3.DetectorSetting) : phiPlusExpectation (LF3.sigmaDotJoint a (reflectXZ b)) = LF3.expectation (LF3.sigmaDotJoint a b)

The two independent Bell derivations agree (the LF6-7 consolidation). The singlet correlation recomputed from Φ⁺ via the xz-reflection transport equals the singlet's own Hilbert-space expectation derived separately in LF3 (LF3.singlet_pauli_correlation): ⟨Φ⁺ | σ·a ⊗ σ·(reflectXZ b) | Φ⁺⟩ = ⟨ψ⁻ | σ·a ⊗ σ·b | ψ⁻⟩. So the symmetric-sector (Φ⁺) computation and the antisymmetric-sector (ψ⁻) computation are the SAME result under reflectXZ — the two independently-derived correlations are one, closing the Φ⁺ ↔ ψ⁻ sector consolidation.

def CSD.LF6.ReproducesPhiPlus {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) (RA RB : LF3.DetectorSetting → Λ → ℝ) : Prop

A product partition reproduces the Φ⁺ (sector) correlations if its factorisable LHV correlation matches Φ⁺'s derived correlation E_{Φ⁺}(a, b) = a_x b_x − a_y b_y + a_z b_z at every pair of settings.

Equations

• CSD.LF6.ReproducesPhiPlus μ RA RB = ∀ (a b : CSD.LF3.DetectorSetting), CSD.Empirical.QM.E91.lhvCorrelation μ RA RB a b = CSD.LF6.phiPlusCorrelation a b

theorem CSD.LF6.no_product_partition_realises_phiPlus {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (RA RB : LF3.DetectorSetting → Λ → ℝ) (hPP : IsProductPartition RA RB) (hRep : ReproducesPhiPlus μ RA RB) : False

no_product_partition_realises_phiPlus (the sector CHSH violation, derived). There is NO product (setting-local, non-contextual) partition of any shared probability space (Λ, μ) whose factorisable correlations reproduce the Bell Φ⁺ correlation function E_{Φ⁺}(a, b) = a_x b_x − a_y b_y + a_z b_z — the correlation of Ψ_d's {0,1}×{0,1} Schmidt sector (maxEntangledSector_eq_phiPlus

• the derived Pauli expectation phiPlus_pauli_correlation).

Genuinely the sector's own violation, not the singlet's imported. A product partition (RA, RB) reproducing Φ⁺ gives, under Bob's xz-axis relabeling RB' := RB ∘ reflectXZ, a product partition reproducing the singlet (phiPlusCorrelation_reflectXZ: E_{Φ⁺}(a, reflectXZ b) = −a·b), contradicting no_product_partition_realises_singlet. The Φ⁺ correlation is a genuine orthogonal relabeling of the singlet's −a·b, so it violates CHSH at the same 2√2 > 2; the violation is derived for Φ⁺, not posited.

theorem CSD.LF6.no_product_partition_realises_maxEntangled (d : ℕ) (hd : 2 ≤ d) : (∀ (i : Fin 2), ∑ j : Fin 2, medWeight d (sectorEmbed d hd i, sectorEmbed d hd j) = (↑d)⁻¹) ∧ maxEntangledSector d hd = ↑(√2 / √↑d) • phiPlus ∧ ∀ (_Λ : Type) [inst : MeasurableSpace _Λ] (μ : MeasureTheory.Measure _Λ) [MeasureTheory.IsProbabilityMeasure μ] (RA RB : LF3.DetectorSetting → _Λ → ℝ), IsProductPartition RA RB → ReproducesPhiPlus μ RA RB → False

no_product_partition_realises_maxEntangled (LF6-D, the thesis-load-bearing non-factorisation, all d ≥ 2). For every d ≥ 2, Ψ_d's {0,1}×{0,1} Schmidt sector IS the Bell Φ⁺ state (coherences included), and NO product (setting-local, non-contextual) partition of any shared probability space (Λ, μ) reproduces that sector's correlation function.

Bell-forced and maxEntangled-specific (derived, not imported). Conjuncts:

• (a) the sector's diagonal Born-weight marginal is uniform 1/d (maxEntangled_sector_marginal_uniform, derived, general d);
• (b) the sector IS Φ⁺ up to the positive scalar √2/√d (maxEntangledSector_eq_phiPlus, full-state identity, coherences included, d-dependent);
• (c) no product partition reproduces the sector's own Φ⁺ correlation function E_{Φ⁺}(a, b) = a_x b_x − a_y b_y + a_z b_z (no_product_partition_realises_phiPlus).

Unlike the earlier revision (which re-exported no_product_partition_realises_singlet verbatim on the singlet's −a·b, an unused d), conjunct (c) is about Φ⁺'s own correlation, which is (i) derived from the Hilbert space (phiPlus_pauli_correlation: ⟨Φ⁺|σ·a ⊗ σ·b|Φ⁺⟩ = a_x b_x − a_y b_y + a_z b_z) and (ii) identified with Ψ_d's sector by (b). The CHSH violation is genuinely Φ⁺'s: an orthogonal relabeling of Bob's axis (reflectXZ) carries E_{Φ⁺} to the singlet's −a·b (phiPlusCorrelation_reflectXZ), so Φ⁺ violates CHSH at the same 2√2 > 2. The non-factorisation is thus Bell-forced and maxEntangled-specific.

Scope: non-factorisation forced by the CHSH-violating 2x2 Φ⁺ sector. This is superseded for every d ≥ 2 by the genuinely d-intrinsic CGLMP violation (CGLMPQudit.no_lhv_realises_maxEntangled_cglmp_d, CGLMPQudit.cglmp_maxEntangled_qudit_gt_two), with d = 3 (CGLMPQutrit.cglmp_maxEntangled_qutrit_gt_two) the concrete qutrit anchor; the general-d CGLMP result is now closed. Residue: SO-1 (the entangled sector posited).

Deliverable 5: the capstone

theorem CSD.LF6.maxEntangledDeisolation_flow_capstone (d : ℕ) [NeZero d] (hd : 2 ≤ d) {M : ℕ} (e : Fin (d * d) × Fin (d * d) ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (LF5.vnDilationV (d * d))) (nudgedMaxEntangled d))) (hψ'0 : ψ' ≠ 0) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN (M + 1)) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : LF5.measurementFlow (d * d) e ≠ id ∧ MeasureTheory.MeasurePreserving (LF5.measurementFlow (d * d) e) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ∧ (∀ (w : Fin d × Fin d), ∑ n : Fin (d * d), ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (n, (medIdx d) w)))).toReal = medWeight d w) ∧ (∀ᵐ (ω : Ω) ∂Pr, ∀ (w : Fin d × Fin d), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin (d * d), (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, (medIdx d) w))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (medWeight d w))) ∧ (∀ (i : Fin 2), ∑ j : Fin 2, medWeight d (sectorEmbed d hd i, sectorEmbed d hd j) = (↑d)⁻¹) ∧ maxEntangledSector d hd = ↑(√2 / √↑d) • phiPlus ∧ ∀ (_Λ : Type) [inst : MeasurableSpace _Λ] (μ : MeasureTheory.Measure _Λ) [MeasureTheory.IsProbabilityMeasure μ] (RA RB : LF3.DetectorSetting → _Λ → ℝ), IsProductPartition RA RB → ReproducesPhiPlus μ RA RB → False

The LF6-D capstone: the general d x d maximally-entangled de-isolation flow. A deterministic, Fubini-Study-measure-preserving de-isolation flow Φ ≠ id on the dilated Σ' = ℂℙ^{d²·d²−1}, for every d ≥ 2, whose context-fixed BornRegion pointer-block volumes are the maximally-entangled Born weights medWeight, with a.s. block frequencies → the weights, plus the derived CHSH-violating 2x2 maximally-entangled sector witness and the Bell-forced non-factorisation. Conjuncts:

1. genuine dynamics, Φ ≠ id (measurementFlow_ne_id, 1 < d*d);
2. physically admissible: FS measure-preserving (measurementFlow_measurePreserving);
3. pointer-block FS volume = the Born weight, every outcome (maxEntangledDeisolation_pointer_volume);
4. a.s. block frequencies → the Born weight (maxEntangledDeisolation_frequency);
5. the 2x2 Schmidt sector's diagonal Born-weight marginal is uniform 1/d (maxEntangled_sector_marginal_uniform, derived, general d);
6. the sector IS the Bell Φ⁺ state up to √2/√d (coherences included, maxEntangledSector_eq_phiPlus, derived, d-dependent);
7. the non-factorisation is Bell-forced and maxEntangled-specific: no setting-local ±1 product partition reproduces the sector's own derived Φ⁺ correlation a_x b_x − a_y b_y + a_z b_z (no_product_partition_realises_phiPlus).

For the strictly stronger, d-intrinsic form of conjunct 7 — non-factorisation forced directly in dimension d by the CGLMP violation cglmp d (pQM d) > 2, with no 2×2 Φ⁺ sector reduction — see maxEntangledDeisolation_flow_capstone_cglmp (LF6/MaxEntangledCGLMPCapstone.lean, fix LF6-1), which inherits conjuncts 1–6 here and swaps only conjunct 7.

Dimension-general (all d ≥ 2): the load-bearing "general-N is now general" content is the de-isolation dynamics + Born-from-volume (conjuncts 1-4). Born = FS-volume is imported from the DH/FS-volume engine, not re-derived; the flow realises (not derives) the measurement. Non-factorisation is Bell-forced via the CHSH-violating 2x2 Φ⁺ sector (conjuncts 5-7): the sector is derived to be Φ⁺ (6), whose two-qubit Pauli correlation is computed (phiPlus_pauli_correlation) and violates CHSH at 2√2 > 2 (7, via the reflectXZ reduction to the singlet). Residue: SO-1 (the entangled sector posited). Honest ledger: module docstring.