LF6-C.3: the GHZ Mermin-context carve (the genuine contextual increment) #

Category: 6-Local (the dynamical realisation of the multipartite entangled de-isolation tier; the D1 entangled frontier at the three-party GHZ Mermin contexts).

This is LF6-C.3 of specs/lf6-plan.md: the genuine contextual increment that C.2 (GHZDeisolationFlow.lean) honestly deferred. Where C.2's minimal computational-basis carve lands on the GHZ diagonal weights and ties to C.1 only by a bare re-export of no_product_partition_realises_ghz, C.3 builds the GHZ Mermin-context carve: the GHZ state in each X/Y measurement basis, whose sign-product-weighted pointer-block Fubini-Study volumes reproduce the four Mermin correlations <XXX> = +1, <XYY> = <YXY> = <YYX> = -1, and the carve ties to C.1 by its OWN achieved correlations (ghzDeisolation_carve_not_product). This is the three-party analogue of A.2's singletDeisolation_blockVolume_correlation + singletDeisolation_carve_not_product.

The new infrastructure (the GHZ Pauli-context joint eigenstructure) #

The corpus carried the singlet joint spin eigenstructure (LF3/Singlet/JointEig) but not its three-party GHZ analogue. This file builds it for the four Mermin contexts. Each context is a triple of Pauli axes ctx : Fin 3 -> PauliAxis; the joint eigenbasis of the product observable sigma.ctx0 (x) sigma.ctx1 (x) sigma.ctx2 is the tensor product of the local X/Y single-qubit eigenstates.

localEig ax o / localAmp : the genuine single-qubit sigma_x / sigma_y eigenstates. localEig_eigenvector proves each is a genuine eigenvector of pauliDot (axisSetting ax) with eigenvalue signC o = ±1. This is what makes the eigenstructure genuine, not a stub.
ghzMerminEig ctx o : the joint eigenstate, the coordinatewise product of the three local amplitudes (the tensor product of genuine local Pauli eigenstates).
ghzMerminEig_born : the Born identity ‖⟨ghz, ghzMerminEig ctx o⟩‖² = (1/16)(1 + signProd o * pv)², where pv = phaseProd ctx is the real context phase product (+1 for XXX, -1 for XYY/YXY/YYX). This is the three-party analogue of singletJointEig_born.

The construction (reusing LF5 @ N = 8 + the new eigenstructure) #

The three-qubit register is measured by the LF5 von Neumann de-isolation flow measurementFlow 8 e on the dilated Σ' = ℂℙ^{63} (64 = 8·8). The prepared state is the GHZ state in the context-ctx basis, nudgedGHZ_mermin ctx, whose computational coordinate at the pointer cell o is ⟨ghz, ghzMerminEig ctx o⟩. Then the headline:

pointer-block o FS volume  =  ‖⟨e_{ghzIdx o}, φ⟩‖²           -- LF5 vnDilation_pointer_volume @ N=8
                           =  ‖⟨ghz, ghzMerminEig ctx o⟩‖²   -- nudge coordinate identity
                           =  (1/16)(1 + signProd o * pv)²   -- ghzMerminEig_born

and the sign-product-weighted block-volume sum ∑_o signProd o · (block o volume) = pv = <ctx> — the Mermin expectation (ghzDeisolation_blockVolume_correlation). Born = FS-volume is imported through vnDilation_pointer_volume (derived one layer down by the moment-map / Duistermaat-Heckman cluster, fs_born_volume_ratio_N, Gleason-free); this file does not re-derive it. What is exercised is the measurement dynamics (Phi != id) plus the new Mermin-context eigenstructure.

The increment over C.2 (the genuine contextual tie) #

C.2's ghzDeisolation_contextuality_anchor is a bare re-export of C.1. C.3's ghzDeisolation_carve_not_product feeds the carve's OWN four achieved Mermin correlations (each a sign-product-weighted sum of bornRegion FS volumes on Σ', discharged to the Mermin value ±1 via ghzDeisolation_blockVolume_correlation) into C.1 no_product_partition_realises_ghz. The four-context tie is closed: no setting-local ±1 product partition reproduces the carve's four correlations, which trigger Mermin's +1 = -1 all-or-nothing contradiction. This is one theorem tying the dynamical carve to C.1, not a juxtaposition.

Honest scope (the C.3 ledger) #

Exhibited. The GHZ Mermin-context carve: for every Mermin context, the pointer-block FS volumes of the LF5 de-isolation flow, sign-product-weighted, equal the Mermin correlation (ghzDeisolation_blockVolume_correlation, all four contexts), tied to C.1 by the carve's own values (ghzDeisolation_carve_not_product, four-context tie closed).
New infrastructure. The GHZ Pauli-context joint eigenstructure (ghzMerminEig, localEig_eigenvector, ghzMerminEig_born) — the three-party analogue of LF3/Singlet/JointEig, built here.
Imported, not re-derived. Born = FS-volume (the DH/moment-map cluster, through vnDilation_pointer_volume). The GHZ Mermin expectations (ghz_expectation_xxx/etc) and the LHV no-go (no_lhv_assignment_for_ghz, C.1) are Empirical.GHZ / LF6-C.1.
Realisation, not derivation. The flow realises the Mermin measurement dynamically; it does not derive the weights from independent dynamics. The carve is the joint moment subdivision, never a setting-local product region. Only the local single-qubit eigen-equation is proved; the tripartite eigen-equation for sigmaDotTriple is the tensor of the three local eigen-equations (definitional, not separately proved).
Residue: SO-1. The GHZ 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, C.1 is measure-theoretic Mermin content).

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

LF6-C.3: the GHZ Mermin-context carve (the genuine contextual increment) #

The new infrastructure (the GHZ Pauli-context joint eigenstructure) #

The construction (reusing LF5 @ N = 8 + the new eigenstructure) #

The increment over C.2 (the genuine contextual tie) #

Honest scope (the C.3 ledger) #

The single-qubit Pauli-axis eigen-amplitudes #

The GHZ Pauli-context joint eigenstructure #

The GHZ inner-product reducer #

The four Mermin contexts and their phase products #

The weight sum / correlation sum algebra #

The nudged GHZ state in the context basis (the prepared state) #

Deliverable: pointer-block FS volume = Mermin block weight #

The headline: the carve's block-volume correlation is the Mermin value #

The dynamical carve-tie to C.1 (the four-context contextuality tie) #

The capstone #