Empirical/CSD: a Mermin–Peres rank-2 observable's outcome Born weights as Kähler volumes #

Category: 3-Local (CSD-ontic volume reading; a quick-win instantiation of the already-proved degenerate-eigenspace engine CSD.Empirical.CSDBridge.ContextVolume.block_born_frequency_volume).

This is the volume-ratio companion to the impossibility readings of the Mermin–Peres magic-square contextuality theorem:

QM side (Empirical/QM/Contextuality/MerminPeres.lean): the six operator-product identities mermin_peres_R0..R2/C0..C2 on the 3×3 two-qubit Pauli grid and the combinatorial no-go no_lhv_mermin_peres.
CSD impossibility side (Empirical/CSD/Contextuality/MerminPeres.lean): no_csd_mermin_peres_assignment — no non-contextual ontic-outcome value assignment to the 9 grid observables is satisfiable.

This file is the complementary volume reading: a single representative grid observable's ±1-outcome Born weights are genuine block sums of Fubini–Study typicality volumes on the fixed ontic Σ = ℂℙ³.

The chosen observable: the non-diagonal `X ⊗ X` #

The diagonal grid observable Z ⊗ Z is already grounded by ContextVolume.zz_parity_born_frequency_volume (computational-basis eigenbasis, no rotation). To complement it we take the most symmetric non-diagonal member, X ⊗ X, whose eigenbasis is H ⊗ H applied to the computational basis — the four product vectors |±⟩ ⊗ |±⟩ with |±⟩ = (|0⟩ ± |1⟩)/√2. With the standard (i, j) ↦ 2i + j flattening of Fin 2 × Fin 2 ≃ Fin 4, X ⊗ X is the anti-diagonal eᵢ ↦ e_{3−i}, so its eigenvectors are the explicit (±1/2)-component rays

v0 = ( 1,  1,  1,  1)/2   eigenvalue +1   (|++⟩)
v1 = ( 1, -1,  1, -1)/2   eigenvalue -1   (|+−⟩)
v2 = ( 1,  1, -1, -1)/2   eigenvalue -1   (|−+⟩)
v3 = ( 1, -1, -1,  1)/2   eigenvalue +1   (|−−⟩)

(the rows of H ⊗ H). Eigenvalue +1 block {v0, v3}, eigenvalue −1 block {v1, v2}: the sign-parity labelling mpXXBlk = ![0, 1, 1, 0] : Fin 4 → Fin 2, identical in shape to the Z ⊗ Z parity grouping. Orthonormality of these explicit (±1/2)-component vectors is a clean norm_num computation (no Cabello-ray transport needed), packaged as mpXXBasis : OrthonormalBasis (Fin 4) ℂ … via OrthonormalBasis.mk + span_eq_top_of_card_eq_finrank.

The eigenbasis identity is proved, not asserted. mpXXVec_eigenvector certifies (σx ⊗ σx) · vᵢ = mpXXEigval i • vᵢ against the genuine Pauli observable sigmaX ⊗ₖ sigmaX of Empirical/QM/Contextuality/MerminPeres.lean (reindexed onto Fin 4 via finProdFinEquiv, where it is the antidiagonal reindex_sigmaXX), and mpXXBlk_eq_zero_iff_eigval_one certifies that the collapsed a = 0 block is exactly the +1 eigenspace. So the headline below lands on the actual σx ⊗ σx = +1 outcome Born weight; the kernel would reject it for any other basis.

The two halves of the Mermin–Peres story, told honestly #

A rank-2 grid observable carries genuine Born weights as block sums of FS typicality volumes. Instantiating block_born_frequency_volume at mpXXBasis, mpXXBlk, and the +1 block, the X ⊗ X = +1 outcome Born weight ⟨ψ, P₊ ψ⟩ = ‖⟨v0, ψ⟩‖² + ‖⟨v3, ψ⟩‖² is the almost-sure limit of empirical frequencies of the block's barycentric Born regions on the fixed ontic Σ = ℂℙ³ — a sum of two Fubini–Study typicality volumes (mp_xx_born_frequency_volume). The −1 block is the identical instantiation at a = 1.
Yet no single non-contextual ±1 assignment is jointly consistent across the square's rows and columns (no_lhv_mermin_peres / no_csd_mermin_peres_assignment, the all-cells-product +1 = −1 impossibility).

The CSD reading of contextuality. Each of the nine grid observables is a rank-2 carving of the one ontic Σ = ℂℙ³; its outcome weights are typicality volumes, recomputed per observable (which orthonormal frame B carves the moment regions). The context-dependence the Mermin–Peres theorem exploits is, on the CSD ontology, the dependence of the carved-volume regions on the measurement frame — not a hidden variable. There is no global section assigning consistent ±1 values across the overlapping row/column contexts, exactly the combinatorial no-go, now sitting beside a genuine per-observable volume realisation.

Scope and honesty #

One representative observable. X ⊗ X is built explicitly; the diagonal Z ⊗ Z is zz_parity_born_frequency_volume. The remaining seven grid observables (Z ⊗ X, X ⊗ Z, Y ⊗ Y, …) are identical instantiations of the same engine at the corresponding H/S-rotated orthonormal frame — no new mathematics; building all nine is mechanical repetition and is omitted.
Realisation, not derivation. As for the whole Empirical/CSD/*Volume series: the Born = FS-volume identity is derived one layer down (the Duistermaat–Heckman / moment-map cluster, LF4.born_frequency_convergence_N_uncond, Gleason-free, no Born put in) and imported here; Φ = id (no dynamics exercised). The Mermin–Peres no-go itself stays at the QM-validity layer (Empirical/QM/).
Gleason-free, foundational-triple-only. The engine is busch_effect_gleason-free; this instantiation inherits that.
No genericity hypothesis. Every unit two-qubit preparation is covered, the computational eigenstates and the Bell states (with vanishing rotated components) included.

cell	frame	eigenvector lemma	volume headline
`X ⊗ I`	`mpHIBasis` (`H ⊗ I`)	`mpXIVec_eigenvector`	`mp_xi_born_frequency_volume`
`I ⊗ X`	`mpIHBasis` (`I ⊗ H`)	`mpIXVec_eigenvector`	`mp_ix_born_frequency_volume`
`X ⊗ X`	`mpXXBasis` (`H ⊗ H`)	`mpXXVec_eigenvector`	`mp_xx_born_frequency_volume`
`I ⊗ Z`	computational	`mpIZVec_eigenvector`	`mp_iz_born_frequency_volume`
`Z ⊗ I`	computational	`mpZIVec_eigenvector`	`mp_zi_born_frequency_volume`
`Z ⊗ Z`	computational	`mpZZVec_eigenvector`	`zz_parity_born_frequency_volume`
`X ⊗ Z`	`mpHIBasis` (`H ⊗ I`)	`mpXZVec_eigenvector`	`mp_xz_born_frequency_volume`
`Z ⊗ X`	`mpIHBasis` (`I ⊗ H`)	`mpZXVec_eigenvector`	`mp_zx_born_frequency_volume`
`Y ⊗ Y`	`mpYYBasis` (`U_Y ⊗ U_Y`)	`mpYYVec_eigenvector`	`mp_yy_born_frequency_volume`

Empirical/CSD: a Mermin–Peres rank-2 observable's outcome Born weights as Kähler volumes #

The chosen observable: the non-diagonal X ⊗ X #

The two halves of the Mermin–Peres story, told honestly #

Scope and honesty #

The X ⊗ X eigenbasis (H ⊗ H) as an OrthonormalBasis #

The eigenbasis identity (machine-checked connection to the real σx ⊗ σx) #

Earning the Z ⊗ Z label for the engine-file zz_parity_born_frequency_volume #

The headline: the X ⊗ X = +1 Born weight as a block sum of FS volumes #

The remaining seven square observables #

The H ⊗ I frame |±⟩ ⊗ eⱼ (shared by X ⊗ I and X ⊗ Z) #

The I ⊗ H frame eᵢ ⊗ |±⟩ (shared by I ⊗ X and Z ⊗ X) #

X ⊗ I (H ⊗ I frame, eigenvalues +1,+1,−1,−1) #

X ⊗ Z (H ⊗ I frame, eigenvalues +1,−1,−1,+1) #

I ⊗ X (I ⊗ H frame, eigenvalues +1,−1,+1,−1) #

Z ⊗ X (I ⊗ H frame, eigenvalues +1,−1,−1,+1) #

Z ⊗ I and I ⊗ Z (computational frame EuclideanSpace.basisFun) #

Y ⊗ Y (the complex U_Y ⊗ U_Y frame |y±⟩ ⊗ |y±⟩) #

Closure: the full nine-observable Mermin–Peres square is grounded #

The chosen observable: the non-diagonal `X ⊗ X` #

The `X ⊗ X` eigenbasis (`H ⊗ H`) as an `OrthonormalBasis` #

The eigenbasis identity (machine-checked connection to the real `σx ⊗ σx`) #

Earning the `Z ⊗ Z` label for the engine-file `zz_parity_born_frequency_volume` #

The headline: the `X ⊗ X = +1` Born weight as a block sum of FS volumes #

The `H ⊗ I` frame `|±⟩ ⊗ eⱼ` (shared by `X ⊗ I` and `X ⊗ Z`) #

The `I ⊗ H` frame `eᵢ ⊗ |±⟩` (shared by `I ⊗ X` and `Z ⊗ X`) #

`X ⊗ I` (`H ⊗ I` frame, eigenvalues `+1,+1,−1,−1`) #

`X ⊗ Z` (`H ⊗ I` frame, eigenvalues `+1,−1,−1,+1`) #

`I ⊗ X` (`I ⊗ H` frame, eigenvalues `+1,−1,+1,−1`) #

`Z ⊗ X` (`I ⊗ H` frame, eigenvalues `+1,−1,−1,+1`) #

`Z ⊗ I` and `I ⊗ Z` (computational frame `EuclideanSpace.basisFun`) #

`Y ⊗ Y` (the complex `U_Y ⊗ U_Y` frame `|y±⟩ ⊗ |y±⟩`) #