LF6-1: the d-intrinsic CGLMP capstone

Category: 6-Local (the d-intrinsic CGLMP capstone).

The general d × d maximally-entangled de-isolation flow capstone (maxEntangledDeisolation_flow_capstone, LF6/MaxEntangledDeisolationFlow.lean) forces non-factorisation through its conjunct 7 via the 2×2 Φ⁺ Schmidt sector — the CHSH violation of the derived Bell state, a genuine force but one that routes through a qubit-sector reduction (no_product_partition_realises_phiPlus).

The CGLMP expert's named follow-on (future-work.md LF6-1) is to reroute that conjunct through the genuinely d-intrinsic CGLMP force: for every d ≥ 2, no local-hidden-variable table (two Bool settings, ZMod d outcomes) reproduces the maximally-entangled QM CGLMP table pQM d, because cglmp d (pQM d) > 2 exceeds the LHV bound 2 DIRECTLY in dimension d (CGLMPQudit.cglmp_maxEntangled_qudit_gt_two, CGLMPQudit.no_lhv_realises_maxEntangled_cglmp_d) — no 2×2 reduction.

Because the CGLMP analytic development (LF6/CGLMPQudit.lean) is downstream of the flow capstone (it imports it, to reuse maxEntangledSector etc.), the reroute cannot edit the original theorem in place without an import cycle. Instead this module states the same capstone with conjunct 7 replaced: maxEntangledDeisolation_flow_capstone_cglmp inherits conjuncts 1–6 verbatim from the flow capstone (dynamics + Born-from-volume + the derived Φ⁺-sector facts) and swaps only conjunct 7 for the d-intrinsic CGLMP force. The Φ⁺/CHSH form remains available as the original theorem's conjunct 7; this is the dimension-intrinsic statement of the same non-factorisation — forced directly in dimension d, with no qubit-sector reduction. (No implication between the two conjunct-7 forms is proved in either direction: they are different formal statements — LHV tables over ZMod d versus product partitions realising Φ⁺ — so neither is claimed "stronger".)

Foundational-triple-only (Gleason-free), like both parents. Residue unchanged: SO-1 (the entangled sector is posited, not derived).

theorem CSD.LF6.maxEntangledDeisolation_flow_capstone_cglmp (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 μ] (A B : Bool → Λ → ZMod d), (∀ (x : Bool), Measurable (A x)) → (∀ (y : Bool), Measurable (B y)) → ProbabilityTheory.CGLMP.lhvTable μ A B = CGLMPQudit.pQM d → False

LF6-1: the d-intrinsic CGLMP capstone. Identical to maxEntangledDeisolation_flow_capstone except its final conjunct (non-factorisation) is rerouted through the general-d CGLMP force instead of the 2×2 Φ⁺/CHSH sector:

1–4. the de-isolation dynamics + Born-from-FS-volume content (Φ ≠ id, FS measure-preserving, pointer-block volume = Born weight, a.s. frequencies → the weight) — inherited verbatim; 5–6. the derived Φ⁺-sector facts (diagonal marginal uniform 1/d; the sector IS the Bell Φ⁺ up to √2/√d) — inherited verbatim; 7. (rerouted) the non-factorisation is Bell-forced d-intrinsically: no local-hidden-variable table (A, B) (two Bool settings, ZMod d outcomes) reproduces the maximally-entangled QM CGLMP table pQM d. This holds because cglmp d (pQM d) > 2 for every d ≥ 2 (cglmp_maxEntangled_qudit_gt_two), a genuine analytic violation in dimension d — no qubit-sector reduction.

Conjuncts 1–6 are discharged by destructuring the flow capstone; conjunct 7 is no_lhv_realises_maxEntangled_cglmp_d.