LF6-C (GHZ_n): the n-party GHZ de-isolation flow and the general-n Mermin forcing

Category: 6-Local (the D1 entangled frontier at general party number; the n-party generalisation of the three-party GHZ C-tier GHZDeisolationFlow.lean / GHZContextuality.lean).

This module carries the deterministic (Mermin) all-or-nothing forcing axis to general party number n, complementing the statistical (CGLMP) axis at general dimension d (MaxEntangledDeisolationFlow.lean + Mathlib/Probability/ CGLMP.lean). Together the two give the symmetric both-axes statement: the de-isolation account reproduces forced non-locality in both the statistical (CGLMP, general d) and deterministic (Mermin/GHZ, general n) forms at arbitrary size. Read this framing against the honest-scope ledger below: the general-n deterministic FORCING (the ±1 combinatorial no-go) is formalised for all n, and (2026-07-03, deliverable 5) the QM link is now ALSO general-n: the four ±1 context targets are DERIVED to be GHZ_n's own tensor-Pauli Mermin correlations ⟨GHZ_n | σ_{a_1} ⊗ … ⊗ σ_{a_n} | GHZ_n⟩ for every n ≥ 3 (ghzN_mermin_correlations), through a genuine two-corner Hilbert reducer (ghzN_expectation_corner), not n = 3-anchored. So "forced non-locality at arbitrary size" is now fully load-bearing (dynamics + forcing + QM link) for general n ≥ 3; the essentially-4-party case is additionally witnessed at n = 4.

What lands

1. ghzN n — the n-qubit GHZ state (|0…0⟩ + |1…1⟩)/√2 on EuclideanSpace ℂ (Fin (2^n)) (all-zeros = 0, all-ones = topIdx n = 2^n−1), ghzNWeight n (Born 1/2 on the two all-equal outcomes, 0 else), unit-norm and weights-sum-one for n ≥ 1. The direct Fin (2^n) generalisation of the three-party ghzWeight.

2. The de-isolation flow + Born-from-volume at N = 2^n (the clean general-party core). ghzNDeisolationFlow n = measurementFlow (2^n) finProdFinEquiv on the dilated Σ' = ℂℙ^{2^n·2^n − 1} (genuinely Φ ≠ id for n ≥ 1, FS-measure-preserving), ghzNDeisolation_pointer_volume (pointer-block FS volume = ghzNWeight, composing LF5 vnDilation_pointer_volume @ N=2^n with the Born identity ghzN_born), _frequency (a.s. block freq → Born), _ne_id, _measurePreserving. This is genuine party-number-general de-isolation dynamics, not tied to n = 3. Born = FS-volume is imported from the DH/ moment-map engine (vnDilation_pointer_volume), not re-derived; the flow realises the measurement, it does not derive the weights.

3. The n-party deterministic (Mermin) forcing (the load-bearing thesis part). no_lhvN_assignment_for_ghzN (general n) and no_product_partition_realises_ghzN (general n) generalise C.1's no_product_partition_realises_ghz to n parties: no setting-local ±1 PRODUCT partition of a shared probability space reproduces the GHZ_n Mermin correlations. The mechanism is the spectator embedding: the three-party Mermin dance runs on parties {0,1,2}, parties ≥ 3 measure X; the full-n product parity contradiction (each party's ±1 value appears squared, so the four correlations multiply to +1 while their product of QM values is −1) is a genuine n-party statement (product over Fin n, n-party contexts). no_lhv_assignment_for_ghz4 is an essentially-four-party witness (all four parties measure Y at least twice; no spectator) via the same parity mechanism.

4. Capstone ghzNDeisolation_flow_capstone (five conjuncts, mirror C.2/LF6-D): Φ ≠ id, FS-measure-preserving, pointer volume = Born, a.s. freq → Born, n-party deterministic no-LHV forcing.

5. The general-n GHZ_n QM tensor-Pauli link (deliverable 5, residual closure). ghzN_expectation_corner (the two-corner Hilbert reducer on Fin (2^n)), tensorPauliFin (the n-fold tensor Pauli via the product-of-factor-entries Kronecker formula on the bit-decomposition basis finFunctionFinEquiv), ghzN_mermin_correlation / ghzN_mermin_correlations (the four GHZ_n Mermin correlations +1, −1, −1, −1 DERIVED for every n ≥ 3, the spectator X-factors contributing +1 via prod_ghzNCtx), and no_product_partition_realises_ghzN_qm (the forcing routed through GHZ_n's ACTUAL QM correlations via reproducesGHZN_QM_iff). This closes the general-n QM-link residual.

Honest scope (the GHZ_n ledger)

• Born imported, not 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. The GHZ_n Born weights are computed from the two amplitudes; this file does not re-derive Born = volume.
• Realisation, not derivation. The flow realises the GHZ_n measurement dynamically; the carve is the joint moment subdivision, never a setting-local product region.
• The forcing is genuine, not posited, not a hollow re-export. The theorem's type genuinely quantifies over n parties, n-party product partitions, and full-n context correlations; the proof is a genuine n-party parity argument. Honest caveat on physical strength: the general-n forcing routes the contradiction through the three-party Mermin paradox embedded via n − 3 X-spectators; it is a valid GHZ_n all-or-nothing but does not exhibit essentially-n-party entanglement beyond three. no_lhv_assignment_for_ghz4 is the essentially-four-party witness (all parties participate) demonstrating genuine beyond-n=3 content. The physical regime is n ≥ 3 (the targets ⟨XXX…⟩ = +1, ⟨XYY…⟩ = −1, … are GHZ_n's actual Mermin correlations for every n ≥ 3, DERIVED here as ghzN_mermin_correlations — deliverable 5, general n; at n = 3 this agrees with Empirical.GHZ.ghz_expectation_*).
• Residue: SO-1. The GHZ_n 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).

Residual (named, honestly)

• The uniform closed-form essentially-all-n-parties general-n Mermin all-or-nothing (which uses every party non-trivially; the construction depends on n mod 4 and is not delivered uniformly here — only the spectator-embedding general-n and the essentially-four-party n = 4 witness are).
• CLOSED (2026-07-03, deliverable 5): the general-n GHZ_n QM confirmation. The four ±1 targets are DERIVED to be the actual ⟨σ_{a_1} ⊗ … ⊗ σ_{a_n}⟩ Mermin correlations for every n ≥ 3 (ghzN_mermin_correlations, via the two-corner reducer ghzN_expectation_corner and the product-of-factor-entries tensor Pauli tensorPauliFin), no longer n = 3-anchored to Empirical.GHZ. The one residual sub-point: the fully-general arbitrary-Pauli-tensor reducer (any Z factors, any axis pattern) is not delivered; only the X/Y Mermin family relevant to the four ghzNCtx contexts is (which is exactly what the forcing consumes).

All exports are foundational-triple-only (Gleason-free; the LF5 pointer engine is off Busch, the forcing is measure-theoretic Mermin content; decide is used only on the two-element PauliAxis inequality x ≠ y (and the n = 4 witness closes by norm_num/ring), no native_decide).

Reference: specs/lf6-plan.md (GHZ_n tranche).

instance CSD.LF6.neZero_two_pow (n : ℕ) : NeZero (2 ^ n)

2 ^ n is nonzero (targeted local instance so the LF5 engine at N = 2^n synthesises [NeZero (2^n)]).

The top computational index 2^n − 1 (all-ones)

def CSD.LF6.topIdx (n : ℕ) : Fin (2 ^ n)

The all-ones computational index 2^n − 1 of Fin (2^n) (the |1…1⟩ support of GHZ_n).

Equations

• CSD.LF6.topIdx n = ⟨2 ^ n - 1, ⋯⟩

theorem CSD.LF6.topIdx_ne_zero (n : ℕ) (hn : n ≠ 0) : topIdx n ≠ 0

For n ≥ 1 the all-ones index is distinct from the all-zeros index 0 (2^n − 1 ≠ 0 since 2^n > 1).

The GHZ_n Born weights

noncomputable def CSD.LF6.ghzNWeight (n : ℕ) (i : Fin (2 ^ n)) : ℝ

The GHZ_n Born weights. The n-qubit GHZ state has support exactly on the two all-equal computational indices 0 (all zeros) and topIdx n (all ones), each with weight 1/2; every other outcome has weight 0. Not a stub: ghzN_normSq_eq_weight proves it equals ‖(ghzN n) i‖².

Equations

• CSD.LF6.ghzNWeight n i = if i = 0 ∨ i = CSD.LF6.topIdx n then 2⁻¹ else 0

The GHZ_n state

noncomputable def CSD.LF6.ghzN (n : ℕ) : EuclideanSpace ℂ (Fin (2 ^ n))

The n-qubit GHZ state (|0…0⟩ + |1…1⟩)/√2 on EuclideanSpace ℂ (Fin (2^n)): computational amplitude (√2)⁻¹ on the all-zeros index 0 and the all-ones index topIdx n, 0 elsewhere. Unit-norm for n ≥ 1. The direct Fin (2^n) generalisation of the three-party ghzState.

Equations

• CSD.LF6.ghzN n = WithLp.toLp 2 fun (i : Fin (2 ^ n)) => if i = 0 ∨ i = CSD.LF6.topIdx n then (↑√2)⁻¹ else 0

theorem CSD.LF6.ghzN_apply (n : ℕ) (i : Fin (2 ^ n)) : (ghzN n).ofLp i = if i = 0 ∨ i = topIdx n then (↑√2)⁻¹ else 0

The computational amplitude of GHZ_n at index i.

theorem CSD.LF6.ghzN_normSq_eq_weight (n : ℕ) (i : Fin (2 ^ n)) : ‖(ghzN n).ofLp i‖ ^ 2 = ghzNWeight n i

The GHZ_n Born weights are the squared computational amplitudes. For every outcome i, ‖(ghzN n) i‖² = ghzNWeight n i — computed from the amplitude (√2)⁻¹ (‖·‖² = 1/2) on the support and the zeros off it.

theorem CSD.LF6.sum_ghzNWeight (n : ℕ) (hn : 0 < n) : ∑ i : Fin (2 ^ n), ghzNWeight n i = 1

The GHZ_n Born weights sum to 1 (two support cells, each 1/2), for n ≥ 1.

theorem CSD.LF6.ghzN_norm (n : ℕ) (hn : 0 < n) : ‖ghzN n‖ = 1

GHZ_n is a unit preparation for n ≥ 1. ‖ghzN n‖² = ∑_i ghzNWeight n i = 1. Discharges the hψ hypothesis of the LF5 pointer-volume / frequency theorems.

theorem CSD.LF6.ghzN_born (n : ℕ) (i : Fin (2 ^ n)) : ‖inner ℂ (EuclideanSpace.single i 1) (ghzN n)‖ ^ 2 = ghzNWeight n i

The GHZ_n coordinate-Born identity. The squared computational amplitude of GHZ_n at pointer cell i equals the Born weight ghzNWeight n i, in the inner ⟨e_i, ·⟩ form the LF5 pointer theorems consume.

Deliverable 2: the de-isolation flow (the clean general-party core)

noncomputable def CSD.LF6.ghzNDeisolationFlow (n : ℕ) : Projectivization ℂ (EuclideanSpace ℂ (Fin (2 ^ n * 2 ^ n))) → Projectivization ℂ (EuclideanSpace ℂ (Fin (2 ^ n * 2 ^ n)))

The GHZ_n de-isolation flow Φ = measurementFlow (2^n) finProdFinEquiv on the dilated projective ontic space Σ' = ℂℙ^{2^n·2^n − 1}. The LF5-B von Neumann de-isolation flow instantiated at the joint n-qubit system N = 2^n.

Equations

• CSD.LF6.ghzNDeisolationFlow n = CSD.LF5.measurementFlow (2 ^ n) finProdFinEquiv

theorem CSD.LF6.ghzNDeisolation_measurePreserving (n : ℕ) (p₀ : LF4.CPN (2 ^ n * 2 ^ n)) : MeasureTheory.MeasurePreserving (ghzNDeisolationFlow n) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

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

theorem CSD.LF6.ghzNDeisolation_ne_id (n : ℕ) (hn : 0 < n) : ghzNDeisolationFlow n ≠ id

The GHZ_n de-isolation flow is genuinely not the identity for n ≥ 1 (1 < 2^n), inherited from measurementFlow_ne_id.

theorem CSD.LF6.ghzNDeisolation_pointer_volume (n : ℕ) (hn : 0 < n) {M : ℕ} (e : Fin (2 ^ n) × Fin (2 ^ n) ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (LF5.vnDilationV (2 ^ n))) (ghzN n))) (hψ'0 : ψ' ≠ 0) (i : Fin (2 ^ n)) : ∑ nn : Fin (2 ^ n), ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (nn, i)))).toReal = ghzNWeight n i

The reproduction (the GHZ_n headline). The context-fixed BornRegion pointer-block i Fubini-Study volume of the GHZ_n de-isolation flow equals the GHZ_n Born weight ghzNWeight n i, for the prepared state φ = ghzN n, every n ≥ 1.

The proof composes LF5 vnDilation_pointer_volume at N = 2^n (pointer-block volume = ‖⟨e_i, φ⟩‖², Gleason-free, Born = FS-volume imported from the DH engine) with the coordinate-Born identity ghzN_born (the computed GHZ_n weights).

theorem CSD.LF6.ghzNDeisolation_frequency (n : ℕ) (hn : 0 < n) {M : ℕ} (e : Fin (2 ^ n) × Fin (2 ^ n) ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (LF5.vnDilationV (2 ^ n))) (ghzN n))) (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, ∀ (i : Fin (2 ^ n)), Filter.Tendsto (fun (m : ℕ) => ∑ nn : Fin (2 ^ n), (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion ψ' hψ'0 (e (nn, i))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (ghzNWeight n i))

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

Deliverable 3: the n-party deterministic (Mermin) forcing

The n-party generalisation of C.1's forced-contextuality no-go (no_product_partition_realises_ghz). The mechanism is the spectator embedding: parties {0,1,2} run the three-party Mermin dance, parties ≥ 3 measure X; the full-n product parity contradiction is a genuine n-party statement.

def CSD.LF6.ghzNCtx (a b c : Empirical.GHZ.PauliAxis) (n : ℕ) (i : Fin n) : Empirical.GHZ.PauliAxis

The n-party Mermin context (a, b, c): party 0 measures Pauli axis a, party 1 axis b, party 2 axis c, every party ≥ 3 (spectator) axis X.

Equations

• CSD.LF6.ghzNCtx a b c n i = if ↑i = 0 then a else if ↑i = 1 then b else if ↑i = 2 then c else CSD.Empirical.GHZ.PauliAxis.x

theorem CSD.LF6.no_lhvN_assignment_for_ghzN (n : ℕ) : ¬∃ (lam : Fin n → Empirical.GHZ.PauliAxis → ℤ), (∀ (i : Fin n) (ax : Empirical.GHZ.PauliAxis), lam i ax = 1 ∨ lam i ax = -1) ∧ ∏ i : Fin n, lam i (ghzNCtx Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.x n i) = 1 ∧ ∏ i : Fin n, lam i (ghzNCtx Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.y n i) = -1 ∧ ∏ i : Fin n, lam i (ghzNCtx Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.y n i) = -1 ∧ ∏ i : Fin n, lam i (ghzNCtx Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.x n i) = -1

No n-party ±1 LHV assignment reproduces the GHZ_n Mermin product constraints (the combinatorial all-or-nothing, general n). The four full-n context products must equal +1 (all-X), −1, −1, −1 (the twisted XYY / YXY / YYX contexts, spectators X); multiplying them, each party's ±1 value appears an even number of times so the product is +1, while the product of the four target values is −1. Contradiction.

Genuinely n-party (product over Fin n, n-party contexts). Physical regime n ≥ 3; the mechanism is the three-party Mermin paradox embedded via n − 3 X-spectators (see the module ledger).

The measure-theoretic n-party forcing (generalising C.1)

theorem CSD.LF6.prod_pm_real {Λ : Type u_1} {n : ℕ} (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ) (c : Fin n → Empirical.GHZ.PauliAxis) (hpm : ∀ (i : Fin n) (ax : Empirical.GHZ.PauliAxis) (l : Λ), R i ax l = 1 ∨ R i ax l = -1) (l : Λ) : ∏ i : Fin n, R i (c i) l = 1 ∨ ∏ i : Fin n, R i (c i) l = -1

The full-n context product of ±1-valued responses is ±1 (its square is 1).

theorem CSD.LF6.prod_meas {Λ : Type u_1} {n : ℕ} [MeasurableSpace Λ] (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ) (c : Fin n → Empirical.GHZ.PauliAxis) (hmeas : ∀ (i : Fin n) (ax : Empirical.GHZ.PauliAxis), Measurable (R i ax)) : Measurable fun (l : Λ) => ∏ i : Fin n, R i (c i) l

The full-n context product is measurable (finite product of measurable responses).

def CSD.LF6.IsProductPartitionGHZN {Λ : Type u_1} [MeasurableSpace Λ] (n : ℕ) (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ) : Prop

R is a product (non-contextual) partition of the shared ontic space (Λ, μ) for the n-party GHZ scenario: R i ax is the ±1 measurable response of party i ∈ Fin n measuring Pauli axis ax ∈ {x, y}, a function of that party's own axis and the shared microstate alone. The n-party analogue of C.1's IsProductPartitionGHZ.

Equations

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

def CSD.LF6.ReproducesGHZN {Λ : Type u_1} [MeasurableSpace Λ] (n : ℕ) (μ : MeasureTheory.Measure Λ) (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ) : Prop

A product partition reproduces the GHZ_n Mermin correlations if its four factorisable full-n context-product expectations match the GHZ_n perfect correlations +1 (all-X), −1, −1, −1 (the twisted contexts). These ±1 targets ARE GHZ_n's actual QM tensor-Pauli Mermin correlations for every n ≥ 3 — DERIVED as ghzN_mermin_correlations (deliverable 5, general n; X⊗ⁿ is a +1 stabiliser, a two-Y-rest-X operator has eigenvalue −1 independent of the spectator count). The forcing is routed through those actual QM correlations by no_product_partition_realises_ghzN_qm (via reproducesGHZN_QM_iff and ReproducesGHZN_QM); the general-n QM link is CLOSED (previously formalised only at n = 3 via Empirical.GHZ).

Equations

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

theorem CSD.LF6.no_product_partition_realises_ghzN {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ) (hPP : IsProductPartitionGHZN n R) (hRep : ReproducesGHZN n μ R) : False

no_product_partition_realises_ghzN (the n-party generalisation of C.1, the load-bearing forcing). There is NO product (setting-local, non-contextual) partition of any shared probability space (Λ, μ) whose factorisable full-n context-product expectations reproduce the GHZ_n Mermin correlations.

Proof (deterministic all-or-nothing, generalising C.1): each of the four ±1-valued full-n product integrands has expectation exactly ±1, so by pm_ae_eq it equals that value μ-a.e.; the four full-measure sets intersect (probability measure), giving a single microstate l₀. Reading off the ±1 value of every party-and-axis response at l₀ yields an n-party deterministic assignment satisfying all four Mermin product constraints, which no_lhvN_assignment_for_ghzN forbids. Genuinely n-party; physical regime n ≥ 3 (see the module ledger).

The essentially-four-party witness (all parties participate)

no_lhv_assignment_for_ghz4 is a genuine four-party all-or-nothing forcing where NO party is a pure spectator: every party measures Y at least twice across the four contexts (YYYY, YXXY, XYXY, XXYY). This is genuine essentially-n-party content beyond the three-party paradox, via the same parity mechanism (the uniform essentially-all-n-parties construction, n mod 4-dependent, is the residual).

theorem CSD.LF6.no_lhv_assignment_for_ghz4 : ¬∃ (lam : Fin 4 → Empirical.GHZ.PauliAxis → ℤ), (∀ (i : Fin 4) (ax : Empirical.GHZ.PauliAxis), lam i ax = 1 ∨ lam i ax = -1) ∧ lam 0 Empirical.GHZ.PauliAxis.y * lam 1 Empirical.GHZ.PauliAxis.y * lam 2 Empirical.GHZ.PauliAxis.y * lam 3 Empirical.GHZ.PauliAxis.y = 1 ∧ lam 0 Empirical.GHZ.PauliAxis.y * lam 1 Empirical.GHZ.PauliAxis.x * lam 2 Empirical.GHZ.PauliAxis.x * lam 3 Empirical.GHZ.PauliAxis.y = -1 ∧ lam 0 Empirical.GHZ.PauliAxis.x * lam 1 Empirical.GHZ.PauliAxis.y * lam 2 Empirical.GHZ.PauliAxis.x * lam 3 Empirical.GHZ.PauliAxis.y = -1 ∧ lam 0 Empirical.GHZ.PauliAxis.x * lam 1 Empirical.GHZ.PauliAxis.x * lam 2 Empirical.GHZ.PauliAxis.y * lam 3 Empirical.GHZ.PauliAxis.y = -1

No four-party ±1 LHV assignment reproduces the essentially-four-party GHZ_4 Mermin constraints. Contexts YYYY (+1), YXXY (−1), XYXY (−1), XXYY (−1); every party has an even (4 or 2) Y/X count, so multiplying the four constraints gives +1 while the product of target values is −1. All four parties participate non-trivially (no spectator).

Deliverable 4: the capstone

theorem CSD.LF6.ghzNDeisolation_flow_capstone (n : ℕ) (hn : 3 ≤ n) {M : ℕ} (e : Fin (2 ^ n) × Fin (2 ^ n) ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (LF5.vnDilationV (2 ^ n))) (ghzN n))) (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 (2 ^ n) e ≠ id ∧ MeasureTheory.MeasurePreserving (LF5.measurementFlow (2 ^ n) e) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ∧ (∀ (i : Fin (2 ^ n)), ∑ nn : Fin (2 ^ n), ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (nn, i)))).toReal = ghzNWeight n i) ∧ (∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin (2 ^ n)), Filter.Tendsto (fun (m : ℕ) => ∑ nn : Fin (2 ^ n), (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion ψ' hψ'0 (e (nn, i))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (ghzNWeight n i))) ∧ ∀ (Λ : Type) [inst : MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ), IsProductPartitionGHZN n R → ReproducesGHZN n μ R → False

The GHZ_n capstone: the n-party GHZ de-isolation flow. A deterministic, Fubini-Study-measure-preserving de-isolation flow Φ ≠ id on the dilated Σ' = ℂℙ^{2^n·2^n − 1}, for every n ≥ 3, whose context-fixed BornRegion pointer-block volumes are the GHZ_n Born weights ghzNWeight, with a.s. block frequencies → the weights, plus the n-party deterministic (Mermin) forcing. Conjuncts:

1. genuine dynamics, Φ ≠ id (measurementFlow_ne_id, 1 < 2^n);
2. physically admissible: FS measure-preserving (measurementFlow_measurePreserving);
3. pointer-block FS volume = the GHZ_n Born weight, every outcome (ghzNDeisolation_pointer_volume);
4. a.s. block frequencies → the GHZ_n Born weight (ghzNDeisolation_frequency);
5. the n-party deterministic forcing: no setting-local ±1 product partition reproduces the GHZ_n Mermin correlations (no_product_partition_realises_ghzN).

Born = FS-volume is imported from the DH/FS-volume engine, not re-derived; the flow realises (not derives) the GHZ_n measurement. The forcing is a genuine n-party statement whose mechanism is the three-party Mermin paradox embedded via X-spectators (no_lhv_assignment_for_ghz4 is the essentially-four-party witness). Residue: SO-1 (the GHZ_n entangled sector posited). Honest ledger: module docstring.

Deliverable 5 (residual closure): the general-n GHZ_n QM tensor-Pauli link

Closes the LF6-E named residual "the general-n GHZ_n QM confirmation that the ±1 targets are the actual ⟨σ_{a_1} ⊗ … ⊗ σ_{a_n}⟩ Mermin correlations". The four ±1 targets of ReproducesGHZN / no_lhvN_assignment_for_ghzN (+1 all-X, −1 for each twisted 2-Y context) are here DERIVED to be GHZ_n's own tensor-Pauli Mermin correlations ⟨GHZ_n | σ_{a_1} ⊗ … ⊗ σ_{a_n} | GHZ_n⟩, for every n ≥ 3, as a genuine Hilbert computation (the two-corner reducer + the product-of-factor-entries tensor Pauli on the bit-decomposition basis), not asserted and not n = 3-anchored.

The tensor-Pauli operator is tensorPauliFin n f, whose (r, c) entry is the standard product-of-factor-entries formula ∏ i, (σ·f i)_{r_i, c_i} under the bit decomposition Fin (2^n) ≃ (Fin n → Fin 2) (finFunctionFinEquiv). This IS the n-fold Kronecker product σ·f₁ ⊗ … ⊗ σ·f_n (the definition of the Kronecker product on the tensor-basis indices); at n = 3 it agrees, up to the Fin 8 ≃ Fin 2 × Fin 2 × Fin 2 reindexing, with Empirical.GHZ.sigmaDotTriple.

The two-corner reducer for GHZ_n on Fin (2^n)

theorem CSD.LF6.sum_two_pow_fin (n : ℕ) : ∑ i : Fin n, 2 ^ ↑i = 2 ^ n - 1

∑ i : Fin n, 2^i = 2^n − 1 (the all-ones binary expansion).

theorem CSD.LF6.ghzN_eq_smul (n : ℕ) (hn : 0 < n) : ghzN n = (↑√2)⁻¹ • (EuclideanSpace.single 0 1 + EuclideanSpace.single (topIdx n) 1)

GHZ_n written as (√2)⁻¹ • (|0…0⟩ + |1…1⟩) in the two-support single-vector form the corner reducer consumes.

theorem CSD.LF6.toELin_single_coord {N : ℕ} (M : Matrix (Fin N) (Fin N) ℂ) (i j : Fin N) : inner ℂ (EuclideanSpace.single i 1) ((Matrix.toEuclideanLin M) (EuclideanSpace.single j 1)) = M i j

Coordinate readout of toEuclideanLin: ⟨e_i, (toEuclideanLin M) e_j⟩ = M i j.

theorem CSD.LF6.ghzN_expectation_corner (n : ℕ) (hn : 0 < n) (M : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ) : inner ℂ (ghzN n) ((Matrix.toEuclideanLin M) (ghzN n)) = 1 / 2 * (M 0 0 + M 0 (topIdx n) + M (topIdx n) 0 + M (topIdx n) (topIdx n))

The two-corner reducer for GHZ_n. For any Fin (2^n)-indexed matrix M, ⟨GHZ_n | M | GHZ_n⟩ reduces to a half-sum over the four corner entries at the two all-equal indices 0 (all zeros) and topIdx n (all ones). A genuine Hilbert computation: GHZ_n is supported on exactly {0, topIdx n}, each with amplitude (√2)⁻¹, so the double sum collapses to the four corner terms, each carrying ((√2)⁻¹)² = 1/2. The Fin (2^n) analogue of Empirical.GHZ.ghz_expectation_formula and phiPlus_expectation_formula.

The tensor-Pauli operator on the bit-decomposition basis

def CSD.LF6.bitDecomp (n : ℕ) (k : Fin (2 ^ n)) : Fin n → Fin 2

The bit decomposition Fin (2^n) → (Fin n → Fin 2) (finFunctionFinEquiv.symm); bitDecomp n k i is the i-th qubit value of the computational index k.

Equations

• CSD.LF6.bitDecomp n k = finFunctionFinEquiv.symm k

theorem CSD.LF6.finFunctionFinEquiv_allZero (n : ℕ) : (finFunctionFinEquiv fun (x : Fin n) => 0) = 0

theorem CSD.LF6.finFunctionFinEquiv_allOne (n : ℕ) : (finFunctionFinEquiv fun (x : Fin n) => 1) = topIdx n

theorem CSD.LF6.bitDecomp_zero_apply (n : ℕ) (i : Fin n) : bitDecomp n 0 i = 0

The all-zeros index bit-decomposes to the all-zeros qubit string.

theorem CSD.LF6.bitDecomp_top_apply (n : ℕ) (i : Fin n) : bitDecomp n (topIdx n) i = 1

The all-ones index topIdx n bit-decomposes to the all-ones qubit string.

noncomputable def CSD.LF6.tensorPauliFin (n : ℕ) (f : Fin n → LF3.DetectorSetting) : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

The n-fold tensor-Pauli operator σ·f₁ ⊗ … ⊗ σ·f_n on Fin (2^n), via the standard product-of-factor-entries Kronecker formula on the bit-decomposition basis: its (r, c) entry is ∏ i, (σ·f i)_{bit r i, bit c i}.

Equations

• CSD.LF6.tensorPauliFin n f = Matrix.of fun (r c : Fin (2 ^ n)) => ∏ i : Fin n, CSD.LF3.pauliDot (f i) (CSD.LF6.bitDecomp n r i) (CSD.LF6.bitDecomp n c i)

theorem CSD.LF6.tensorPauliFin_apply (n : ℕ) (f : Fin n → LF3.DetectorSetting) (r c : Fin (2 ^ n)) : tensorPauliFin n f r c = ∏ i : Fin n, LF3.pauliDot (f i) (bitDecomp n r i) (bitDecomp n c i)

The single-qubit axis assignment and its Pauli entries

noncomputable def CSD.LF6.axisVec : Empirical.GHZ.PauliAxis → LF3.DetectorSetting

The measurement axis as a DetectorSetting: x ↦ chshA = (1,0,0) (σ_x), y ↦ chshA' = (0,1,0) (σ_y).

Equations

• CSD.LF6.axisVec CSD.Empirical.GHZ.PauliAxis.x = CSD.Empirical.Bell.chshA
• CSD.LF6.axisVec CSD.Empirical.GHZ.PauliAxis.y = CSD.Empirical.Bell.chshA'

theorem CSD.LF6.pauliDot_axisVec_00 (ax : Empirical.GHZ.PauliAxis) : LF3.pauliDot (axisVec ax) 0 0 = 0

(σ·axisVec ax)_{0,0} = a_z = 0 (both σ_x, σ_y are traceless, z-free).

theorem CSD.LF6.pauliDot_axisVec_11 (ax : Empirical.GHZ.PauliAxis) : LF3.pauliDot (axisVec ax) 1 1 = 0

(σ·axisVec ax)_{1,1} = −a_z = 0.

theorem CSD.LF6.pauliDot_axisVec_01 (ax : Empirical.GHZ.PauliAxis) : LF3.pauliDot (axisVec ax) 0 1 = if ax = Empirical.GHZ.PauliAxis.y then -Complex.I else 1

The (0,1) corner entry: 1 for X, −i for Y (a_x − i a_y).

theorem CSD.LF6.pauliDot_axisVec_10 (ax : Empirical.GHZ.PauliAxis) : LF3.pauliDot (axisVec ax) 1 0 = if ax = Empirical.GHZ.PauliAxis.y then Complex.I else 1

The (1,0) corner entry: 1 for X, i for Y (a_x + i a_y).

The GHZ_n tensor-Pauli expectation and the four Mermin correlations

noncomputable def CSD.LF6.ghzNPauliExpectation (n : ℕ) (c : Fin n → Empirical.GHZ.PauliAxis) : ℂ

The GHZ_n tensor-Pauli expectation for a context c : Fin n → PauliAxis: ⟨GHZ_n | σ·(axisVec (c 0)) ⊗ … ⊗ σ·(axisVec (c (n−1))) | GHZ_n⟩.

Equations

• CSD.LF6.ghzNPauliExpectation n c = inner ℂ (CSD.LF6.ghzN n) ((Matrix.toEuclideanLin (CSD.LF6.tensorPauliFin n fun (i : Fin n) => CSD.LF6.axisVec (c i))) (CSD.LF6.ghzN n))

theorem CSD.LF6.ghzNPauliExpectation_eq (n : ℕ) (hn : 0 < n) (c : Fin n → Empirical.GHZ.PauliAxis) : ghzNPauliExpectation n c = 1 / 2 * (∏ i : Fin n, LF3.pauliDot (axisVec (c i)) 0 1 + ∏ i : Fin n, LF3.pauliDot (axisVec (c i)) 1 0)

The GHZ_n expectation reduces to the two off-diagonal corner products. For every context of X/Y axes and every n ≥ 1, ⟨GHZ_n | ⊗σ | GHZ_n⟩ = (1/2)(∏_i (σ·axisVec (c i))_{0,1} + ∏_i (σ·axisVec (c i))_{1,0}). The (0,0) and (1,1) corner products vanish (each factor = a_z = 0); the surviving two are the (0,1)/(1,0) products. Genuine Hilbert computation via ghzN_expectation_corner.

theorem CSD.LF6.prod_ghzNCtx {F : Empirical.GHZ.PauliAxis → ℂ} (hF : F Empirical.GHZ.PauliAxis.x = 1) (a b c : Empirical.GHZ.PauliAxis) (n : ℕ) (hn : 3 ≤ n) : ∏ i : Fin n, F (ghzNCtx a b c n i) = F a * F b * F c

Spectator collapse. For a context (a on party 0, b on party 1, c on party 2, X on every spectator party ≥ 3) and any factor function F with F x = 1, the full-n product collapses to the three essential parties: ∏_i F(ghzNCtx a b c n i) = F a · F b · F c, for every n ≥ 3. This is what makes the n − 3 X-spectators contribute +1 and the general-n correlation match the three-party Mermin value.

theorem CSD.LF6.ghzN_mermin_correlation (n : ℕ) (hn : 3 ≤ n) (a b c : Empirical.GHZ.PauliAxis) : ghzNPauliExpectation n (ghzNCtx a b c n) = 1 / 2 * ((((if a = Empirical.GHZ.PauliAxis.y then -Complex.I else 1) * if b = Empirical.GHZ.PauliAxis.y then -Complex.I else 1) * if c = Empirical.GHZ.PauliAxis.y then -Complex.I else 1) + ((if a = Empirical.GHZ.PauliAxis.y then Complex.I else 1) * if b = Empirical.GHZ.PauliAxis.y then Complex.I else 1) * if c = Empirical.GHZ.PauliAxis.y then Complex.I else 1)

The GHZ_n Mermin correlation (general n). For a Mermin context (a, b, c) with X-spectators, `⟨GHZ_n | ⊗σ | GHZ_n⟩ = (1/2)(g₀₁ a · g₀₁ b · g₀₁ c

• g₁₀ a · g₁₀ b · g₁₀ c), where g₀₁ = (1, −i)on(X, Y)andg₁₀ = (1, i). Derived from ghzNPauliExpectation_eq+prod_ghzNCtx, every n ≥ 3`.

theorem CSD.LF6.ghzN_correlation_allX (n : ℕ) (hn : 3 ≤ n) : ghzNPauliExpectation n (ghzNCtx Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.x n) = 1

GHZ_n ⟨XXX…X⟩ = +1 (all-X context, general n ≥ 3). Mermin identity #1, GHZ_n's own tensor-Pauli correlation.

theorem CSD.LF6.ghzN_correlation_xyy (n : ℕ) (hn : 3 ≤ n) : ghzNPauliExpectation n (ghzNCtx Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.y n) = -1

GHZ_n ⟨XYY…⟩ = −1 (twisted X,Y,Y context, X-spectators, general n ≥ 3). Mermin identity #2; n_y = 2, cos(π) = −1.

theorem CSD.LF6.ghzN_correlation_yxy (n : ℕ) (hn : 3 ≤ n) : ghzNPauliExpectation n (ghzNCtx Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.y n) = -1

GHZ_n ⟨YXY…⟩ = −1 (twisted Y,X,Y context, general n ≥ 3). Mermin identity #3.

theorem CSD.LF6.ghzN_correlation_yyx (n : ℕ) (hn : 3 ≤ n) : ghzNPauliExpectation n (ghzNCtx Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.x n) = -1

GHZ_n ⟨YYX…⟩ = −1 (twisted Y,Y,X context, general n ≥ 3). Mermin identity #4.

theorem CSD.LF6.ghzN_mermin_correlations (n : ℕ) (hn : 3 ≤ n) : ghzNPauliExpectation n (ghzNCtx Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.x n) = 1 ∧ ghzNPauliExpectation n (ghzNCtx Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.y n) = -1 ∧ ghzNPauliExpectation n (ghzNCtx Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.x Empirical.GHZ.PauliAxis.y n) = -1 ∧ ghzNPauliExpectation n (ghzNCtx Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.y Empirical.GHZ.PauliAxis.x n) = -1

The four GHZ_n Mermin correlations, general n ≥ 3 (the residual-closing bundle). ⟨XXX…⟩ = +1, ⟨XYY…⟩ = −1, ⟨YXY…⟩ = −1, ⟨YYX…⟩ = −1 are GHZ_n's OWN tensor-Pauli correlations, for every n ≥ 3 — the four ±1 targets of ReproducesGHZN / no_lhvN_assignment_for_ghzN. Genuine derived Hilbert computations, not n = 3-anchored.

Routing the forcing through GHZ_n's actual QM correlations

def CSD.LF6.ReproducesGHZN_QM {Λ : Type u_1} [MeasurableSpace Λ] (n : ℕ) (μ : MeasureTheory.Measure Λ) (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ) : Prop

A product partition reproduces GHZ_n's ACTUAL QM tensor-Pauli Mermin correlations: its four factorisable full-n context-product expectations match (ghzNPauliExpectation n …).re, i.e. the genuine ⟨GHZ_n | ⊗σ | GHZ_n⟩. Unlike ReproducesGHZN (bare ±1 numerals), the targets here are GHZ_n's own derived Hilbert correlations.

Equations

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

theorem CSD.LF6.reproducesGHZN_QM_iff {Λ : Type u_1} [MeasurableSpace Λ] (n : ℕ) (hn : 3 ≤ n) (μ : MeasureTheory.Measure Λ) (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ) : ReproducesGHZN_QM n μ R ↔ ReproducesGHZN n μ R

The QM link (general n ≥ 3): the ±1 targets ARE GHZ_n's QM correlations. ReproducesGHZN_QM n μ R ↔ ReproducesGHZN n μ R, because GHZ_n's four tensor-Pauli Mermin correlations are exactly +1, −1, −1, −1 (ghzN_mermin_correlations). This is the residual closure: the abstract ±1 targets of the forcing are GHZ_n's OWN QM correlations, for every n ≥ 3, not just n = 3.

theorem CSD.LF6.no_product_partition_realises_ghzN_qm {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) (hn : 3 ≤ n) (R : Fin n → Empirical.GHZ.PauliAxis → Λ → ℝ) (hPP : IsProductPartitionGHZN n R) (hRep : ReproducesGHZN_QM n μ R) : False

no_product_partition_realises_ghzN_qm (the residual-closed forcing, general n ≥ 3). No product (setting-local, non-contextual) partition of any shared probability space reproduces GHZ_n's ACTUAL QM tensor-Pauli Mermin correlations ⟨GHZ_n | ⊗σ | GHZ_n⟩ (the .re values +1, −1, −1, −1). Routes the LF6-E forcing no_product_partition_realises_ghzN through GHZ_n's own derived QM correlations (reproducesGHZN_QM_iff), so the general-n GHZ_n non-locality is genuinely GHZ_n-specific and not n = 3-anchored.