LF6-C.1: Forced contextuality of the GHZ state (the multipartite tier crux)

Category: 6-Local (the first general-N-tier instance of CSD's D1 entangled frontier; the multipartite analogue of LF6-A.1's singlet forced-contextuality crux).

Glossary: https://glossary.constraintsurfacedynamics.com/ghz-state/ Plain-language, CSD-role and formal statements of the GHZ state, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The idea

LF6-A.1 (ForcedContextuality.lean) showed: a product (setting-local, non-contextual) outcome-partition of the ontic space on a shared probability space (Λ, μ) is a deterministic local-hidden-variable model, and by Bell/CHSH no such partition reproduces the singlet correlations; so any de-isolation carve realising the singlet is jointly contextual. The forcing there is statistical: the LHV CHSH cap |S| <= 2 versus the singlet 2 sqrt 2.

This file is the GHZ analogue. The three-qubit GHZ state forces contextuality deterministically: the four perfect correlations

<XXX> = +1,  <XYY> = -1,  <YXY> = -1,  <YYX> = -1

admit NO consistent local plus/minus 1 value assignment at all (Mermin's all-or-nothing paradox), because the product of the four constraints forces +1 = -1 once each squared plus/minus 1 value is 1. There is no inequality and no statistics in the contradiction: a single shared assignment is already impossible. This is a qualitatively stronger and structurally different forcing than the singlet's CHSH bound.

What is reused (no GHZ re-proof, no Bell/kernel reinvention)

• CSD.Empirical.GHZ.no_lhv_assignment_for_ghz: the deterministic all-or-nothing no-go (no plus/minus 1 assignment satisfies the four Mermin product constraints). no_product_partition_realises_ghz routes through it; it does NOT re-prove the GHZ paradox.
• CSD.Empirical.GHZ.ghz_expectation_xxx (= +1) and ghz_expectation_formula (the half-sum corner reducer), for the engine non-factorisation / marginal pair.

The deterministic forcing mechanism (the genuine increment over A.1)

A product partition is a triple of setting-local plus/minus 1 responses on a shared (Λ, μ), one per wing. If it reproduces the GHZ correlations (the four perfect expectations above), then each plus/minus 1 valued product integrand has expectation exactly plus/minus 1 on a probability space, which forces it to equal that value mu-almost-everywhere. Intersecting the four full-measure sets yields a single microstate l0 carrying a deterministic plus/minus 1 value for every wing-and-axis setting, satisfying all four Mermin constraints simultaneously: exactly the assignment no_lhv_assignment_for_ghz forbids. The contradiction is reached at one point, not through an inequality.

Conceptual ledger (honest)

• Deterministic, not statistical. Contrast A.1's |S| <= 2 versus 2 sqrt 2 margin. Here the contradiction is single-shot and algebraic: no LHV at all.
• plus/minus 1 AND locality both load-bearing. ReproducesGHZ is stated statistically (expectations), so the plus/minus 1 hypothesis is what upgrades "expectation = plus/minus 1" to "pointwise determinism": with unconstrained real responses an expectation of plus/minus 1 does not force a definite value. Locality (a single shared assignment across the four contexts) is the other load-bearing leg: ghz_each_correlation_locally_realisable shows each of the four correlations is individually realisable by a local plus/minus 1 assignment; only realising all four with ONE assignment fails. So the impossibility is the non-contextual locality plus the two-valuedness, not any single correlation.
• One engine, two outputs. The Born weights (LF4/LF5 moment-map volume, imported, not re-derived) and the non-factorisation (this file) are two readings of the same Sigma-volume engine. ghz_engine_marginal_factorises (each single-wing marginal = 0, maximally mixed, no-signalling) holds even though the joint <XXX> does not factor (ghz_engine_joint_nonfactorises).
• Residue: SO-1. This realises the GHZ correlations MODULO the posited CSD sector (SO-1): the GHZ entangled sector / preparation region is posited, not derived from deterministic dynamics (SO-1: the sector origin, distinct from Paper C Axiom A5). Same posture as the singlet (A.1).
• Scope: C.1 only. THIS file is the forced-contextuality crux. The full GHZ de-isolation FLOW on the dilated three-qubit space (a deterministic FS-measure-preserving Phi != id whose pointer-block volumes are the GHZ Born weights, mirroring A.2/A.3) is LF6-C.2, deferred.

All exports are foundational-triple-only (the machinery is measure-theoretic; no Busch, no decide on the headline).

plus/minus 1 arithmetic and integrability helpers

theorem CSD.LF6.pm_mul {a b : ℝ} (ha : a = 1 ∨ a = -1) (hb : b = 1 ∨ b = -1) : a * b = 1 ∨ a * b = -1

A product of two plus/minus 1 reals is plus/minus 1.

The product-partition predicate (three-wing analogue of A.1)

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

R is a product (non-contextual) partition of the shared ontic space (Λ, μ) for the three-party GHZ scenario: R i ax is the plus/minus 1 measurable response of wing i in Fin 3 measuring Pauli axis ax in {x, y}, a function of that wing's own axis and the shared microstate alone. The setting-locality on a shared Λ is exactly the non-contextual local-hidden-variable assumption.

Equations

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

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

A product partition reproduces the GHZ correlations if its four factorisable wing-product expectations match the four GHZ perfect correlations <XXX> = +1, <XYY> = <YXY> = <YYX> = -1.

Equations

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

The deterministic forced-contextuality no-go (THE headline)

theorem CSD.LF6.no_product_partition_realises_ghz {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] (R : Fin 3 → Empirical.GHZ.PauliAxis → Λ → ℝ) (hPP : IsProductPartitionGHZ R) (hRep : ReproducesGHZ μ R) : False

no_product_partition_realises_ghz (LF6-C.1, load-bearing). There is NO product (setting-local, non-contextual) partition of any shared probability space (Λ, μ) whose factorisable wing-product expectations reproduce the four GHZ perfect correlations.

Proof (DETERMINISTIC, all-or-nothing): each of the four plus/minus 1 valued product integrands has expectation exactly plus/minus 1, so by pm_ae_eq it equals that value mu-a.e.; the four full-measure sets intersect (probability measure), giving a single microstate l0. Reading off the plus/minus 1 value of every wing-and-axis response at l0 yields a deterministic assignment Fin 3 -> PauliAxis -> Z satisfying all four Mermin constraints, which no_lhv_assignment_for_ghz forbids. The contradiction is at one point, not a statistical inequality (contrast A.1's 2 < 2 sqrt 2).

Routes through CSD.Empirical.GHZ.no_lhv_assignment_for_ghz; it does NOT re-prove the GHZ paradox.

theorem CSD.LF6.productPartition_ghz_nonvacuous {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] : (IsProductPartitionGHZ fun (x : Fin 3) (x_1 : Empirical.GHZ.PauliAxis) (x_2 : Λ) => 1) ∧ ∫ (x : Λ), 1 * 1 * 1 ∂μ = 1

Non-vacuity of the no-go. Product partitions exist: the all-plus 1 responses form a product partition. Its <XXX> correlation integral is 1, matching the GHZ value, so the predicate is inhabited and reproduces SOME of the GHZ data; but it cannot meet the three -1 constraints (its products are constantly 1), so no_product_partition_realises_ghz is a genuine separation, not a vacuous predicate.

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

Locality is load-bearing. Each of the four GHZ correlations is, on its own, realisable by a local plus/minus 1 assignment: the +1 constraint by the all-plus 1 assignment, each -1 constraint by flipping wing 0. Only realising all four with ONE shared (non-contextual) assignment is impossible. This isolates the load-bearing structure in no_product_partition_realises_ghz: the contradiction is the non-contextual locality plus the two-valuedness, not any individual correlation value being unattainable.

The engine's non-factorising joint / factorising marginal pair

The GHZ analogue of A.1's engine_joint_nonfactorises / engine_marginal_factorises. The single-wing marginal observables (one Pauli, two identities) all have GHZ expectation 0: the marginals factor (each wing maximally mixed, no-signalling), while the joint <XXX> = 1 does not factor.

noncomputable def CSD.LF6.margWing0 (a : LF3.DetectorSetting) : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

Single-wing marginal observable (sigma . a) tensor I tensor I (wing 0).

Equations

• CSD.LF6.margWing0 a = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CSD.LF3.pauliDot a) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 1)

noncomputable def CSD.LF6.margWing1 (a : LF3.DetectorSetting) : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

Single-wing marginal observable I tensor (sigma . a) tensor I (wing 1).

Equations

• CSD.LF6.margWing1 a = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CSD.LF3.pauliDot a) 1)

noncomputable def CSD.LF6.margWing2 (a : LF3.DetectorSetting) : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

Single-wing marginal observable I tensor I tensor (sigma . a) (wing 2).

Equations

• CSD.LF6.margWing2 a = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (CSD.LF3.pauliDot a))

theorem CSD.LF6.ghz_marginal_wing0 (a : LF3.DetectorSetting) (haz : a.vec.ofLp 2 = 0) : (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing0 a)) Empirical.GHZ.ghzState)).re = 0

Wing-0 marginal of GHZ vanishes for any axis with a_z = 0 (X or Y).

theorem CSD.LF6.ghz_marginal_wing1 (a : LF3.DetectorSetting) (haz : a.vec.ofLp 2 = 0) : (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing1 a)) Empirical.GHZ.ghzState)).re = 0

Wing-1 marginal of GHZ vanishes for any axis with a_z = 0 (X or Y).

theorem CSD.LF6.ghz_marginal_wing2 (a : LF3.DetectorSetting) (haz : a.vec.ofLp 2 = 0) : (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing2 a)) Empirical.GHZ.ghzState)).re = 0

Wing-2 marginal of GHZ vanishes for any axis with a_z = 0 (X or Y).

theorem CSD.LF6.ghz_engine_joint_nonfactorises : (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (Empirical.GHZ.sigmaDotTriple Empirical.Bell.chshA Empirical.Bell.chshA Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re ≠ (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing0 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re * (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing1 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re * (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing2 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re

ghz_engine_joint_nonfactorises. The GHZ joint correlation <XXX> = 1 does NOT factor into the product of the single-wing X-marginals (each 0): 1 != 0 * 0 * 0. The Sigma-volume engine's non-factorising joint.

theorem CSD.LF6.ghz_engine_marginal_factorises : (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing0 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re = 0 ∧ (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing1 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re = 0 ∧ (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing2 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re = 0 ∧ (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing0 Empirical.Bell.chshA')) Empirical.GHZ.ghzState)).re = 0 ∧ (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing1 Empirical.Bell.chshA')) Empirical.GHZ.ghzState)).re = 0 ∧ (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing2 Empirical.Bell.chshA')) Empirical.GHZ.ghzState)).re = 0

ghz_engine_marginal_factorises (no-signalling). Each single-wing marginal of GHZ is 0 (maximally mixed), for both the X and Y axes on every wing, independent of the other wings' settings. The marginals factor even though the joint does not.

theorem CSD.LF6.ghz_forced_contextuality_capstone {Λ : Type u_1} [MeasurableSpace Λ] (μ : MeasureTheory.Measure Λ) [MeasureTheory.IsProbabilityMeasure μ] : (∀ (R : Fin 3 → Empirical.GHZ.PauliAxis → Λ → ℝ), IsProductPartitionGHZ R → ¬ReproducesGHZ μ R) ∧ (IsProductPartitionGHZ fun (x : Fin 3) (x_1 : Empirical.GHZ.PauliAxis) (x_2 : Λ) => 1) ∧ (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (Empirical.GHZ.sigmaDotTriple Empirical.Bell.chshA Empirical.Bell.chshA Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re ≠ (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing0 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re * (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing1 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re * (inner ℂ Empirical.GHZ.ghzState ((Matrix.toEuclideanLin (margWing2 Empirical.Bell.chshA)) Empirical.GHZ.ghzState)).re

Capstone (LF6-C.1). The forced-contextuality crux for GHZ: no product (non-contextual, three-wing-local) partition reproduces the GHZ correlations (deterministic all-or-nothing forcing), product partitions exist, and the joint <XXX> does not factor into the single-wing marginals.