LF4 §14.2 at N = 4: two-qubit Pauli observables on the singlet preparation

Category: 3-Local (LF4 §14.2 extension to N = 4 — two-qubit Pauli spectral decomposition on the singlet Σ = ℂℙ³ × T² instance).

Lifts the §14.2 single-qubit Pauli pattern (SingleQubitKahler.lean, pauliDot_observable_correspondence) to the three two-qubit Pauli forms on the singlet preparation:

• σ·a ⊗ I (left wing) — sigmaDotLeftOntic,
• I ⊗ σ·b (right wing) — sigmaDotRightOntic,
• σ·a ⊗ σ·b (joint) — sigmaDotJointOntic.

Each observable has eigenvalues ±1 with rank-2 eigenspaces in the 4-dimensional 2-qubit space. The spectral decomposition over the existing four singlet sectors kRegion ctx s t gives the ontic counterpart as an eigenvalue-weighted sum of sector indicators.

§14.2 correspondence for the three forms

Form	Eigenvalue weight on sector (s,t)	Integral against kMuPsi	Singlet expectation
σ·a ⊗ I	s.val	0	0
I ⊗ σ·b	t.val	0	0
σ·a ⊗ σ·b	s.val · t.val	−a·b	−a·b

Both sides of each correspondence theorem land on the same value via independent routes:

• Hilbert side: the existing LF3 singlet-expectation theorems (singlet_left/right_pauli_expectation_zero, singlet_pauli_correlation).
• Ontic side: sector-marginal/correlation identities from LF3 (marginal_a_eq_half, marginal_b_eq_half, context_correlation_eq_neg_dot), integrated through kMuPsi_kRegion (the singlet sector carving identity).

Why this gives Mermin–Peres for free

Each of the nine Mermin–Peres 3×3-grid observables is an instance of one of the three forms (σ_a ⊗ I, I ⊗ σ_b, or σ_a ⊗ σ_b for appropriate axes). The §14.2 correspondence theorems below give the per-observable Hilbert ↔ ontic match. Combined with the existing MP combinatorial impossibility (Empirical/QM/Contextuality/MerminPeres.lean's no_lhv_mermin_peres and mermin_peres_R0..R2, C0..C2), the contextuality proof is now available at the LF3-chain level.

For Hardy, three of the four observables (the single-qubit Paulis on each side) are instances of sigmaDotLeft and sigmaDotRight. The full Hardy joint-frequency lift additionally requires per-Hardy-context preparations and joint outcome regions; that is a follow-up tranche.

Tier-2 honesty (unchanged)

The singlet sector regions kRegion ctx s t are carved to volume P_st ctx.a ctx.b s t by construction. The §14.2 integration identities hold because Hilbert and ontic sides equal the same prescribed values through independent routes. Not a derivation; faithful realisation.

Axiom posture

Foundational triple only. Reuses kRegion_measurable, kMuPsi_kRegion from SingletKahler.lean; reuses the LF3 marginal/correlation algebra.

Algebraic helpers: sector-weighted P_st sums

theorem CSD.LF4.sum_sign_val : ∑ s : LF3.Sign, s.val = 0

theorem CSD.LF4.sum_sectorLeft_PSt_eq_zero (a b : LF3.DetectorSetting) : ∑ st : LF3.Sign × LF3.Sign, st.1.val * LF3.P_st a b st.1 st.2 = 0

theorem CSD.LF4.sum_sectorRight_PSt_eq_zero (a b : LF3.DetectorSetting) : ∑ st : LF3.Sign × LF3.Sign, st.2.val * LF3.P_st a b st.1 st.2 = 0

The three §14.2 ontic counterparts

noncomputable def CSD.LF4.sigmaDotLeftOntic (ctx : LF3.MeasurementContext) (σ : KSigma 4) : ℝ

Ontic counterpart of σ·a ⊗ I on the singlet: signed-indicator over the four singlet sectors, weighted by the left sign of each sector (s, t).

Equations

• CSD.LF4.sigmaDotLeftOntic ctx σ = ∑ st : CSD.LF3.Sign × CSD.LF3.Sign, st.1.val * (CSD.LF4.kRegion ctx st.1 st.2).indicator (fun (x : CSD.LF4.KSigma 4) => 1) σ

noncomputable def CSD.LF4.sigmaDotRightOntic (ctx : LF3.MeasurementContext) (σ : KSigma 4) : ℝ

Ontic counterpart of I ⊗ σ·b on the singlet: signed by the right sign of each sector.

Equations

• CSD.LF4.sigmaDotRightOntic ctx σ = ∑ st : CSD.LF3.Sign × CSD.LF3.Sign, st.2.val * (CSD.LF4.kRegion ctx st.1 st.2).indicator (fun (x : CSD.LF4.KSigma 4) => 1) σ

noncomputable def CSD.LF4.sigmaDotJointOntic (ctx : LF3.MeasurementContext) (σ : KSigma 4) : ℝ

Ontic counterpart of σ·a ⊗ σ·b on the singlet: signed by the product of the sector signs.

Equations

• CSD.LF4.sigmaDotJointOntic ctx σ = ∑ st : CSD.LF3.Sign × CSD.LF3.Sign, st.1.val * st.2.val * (CSD.LF4.kRegion ctx st.1 st.2).indicator (fun (x : CSD.LF4.KSigma 4) => 1) σ

Integration identities (§14.2 ontic-side values)

theorem CSD.LF4.indicator_kRegion_integrable (ctx : LF3.MeasurementContext) (s t : LF3.Sign) : MeasureTheory.Integrable ((kRegion ctx s t).indicator fun (x : KSigma 4) => 1) kMuPsi

For each sector, the indicator of kRegion ctx s t is integrable against kMuPsi.

theorem CSD.LF4.weighted_indicator_sum_integral (ctx : LF3.MeasurementContext) (w : LF3.Sign × LF3.Sign → ℝ) : ∫ (σ : KSigma 4), ∑ st : LF3.Sign × LF3.Sign, w st * (kRegion ctx st.1 st.2).indicator (fun (x : KSigma 4) => 1) σ ∂kMuPsi = ∑ st : LF3.Sign × LF3.Sign, w st * LF3.P_st ctx.a ctx.b st.1 st.2

The integral of a sector-weighted indicator sum is the corresponding P_st-weighted scalar sum. The shared computational step underlying all three §14.2 forms.

theorem CSD.LF4.sigmaDotLeftOntic_integral (ctx : LF3.MeasurementContext) : ∫ (σ : KSigma 4), sigmaDotLeftOntic ctx σ ∂kMuPsi = 0

σ·a ⊗ I ontic integral. Vanishes by the left marginal Σ_t P_st = 1/2 and Σ_s s.val = 0.

theorem CSD.LF4.sigmaDotRightOntic_integral (ctx : LF3.MeasurementContext) : ∫ (σ : KSigma 4), sigmaDotRightOntic ctx σ ∂kMuPsi = 0

I ⊗ σ·b ontic integral. Vanishes by the right marginal.

theorem CSD.LF4.sigmaDotJointOntic_integral (ctx : LF3.MeasurementContext) : ∫ (σ : KSigma 4), sigmaDotJointOntic ctx σ ∂kMuPsi = -LF3.dotR ctx.a ctx.b

σ·a ⊗ σ·b ontic integral. Equals −a·b via the LF3 singlet correlation context_correlation_eq_neg_dot.

Observable correspondence theorems (§14.2 at N = 4)

theorem CSD.LF4.sigmaDotLeft_observable_correspondence (ctx : LF3.MeasurementContext) : LF3.expectation (LF3.sigmaDotLeft ctx.a) = ↑(∫ (σ : KSigma 4), sigmaDotLeftOntic ctx σ ∂kMuPsi)

§14.2 observable correspondence for σ·a ⊗ I on the singlet. Both sides equal 0: the Hilbert side via singlet_left_pauli_expectation_zero, the ontic side via sigmaDotLeftOntic_integral.

theorem CSD.LF4.sigmaDotRight_observable_correspondence (ctx : LF3.MeasurementContext) : LF3.expectation (LF3.sigmaDotRight ctx.b) = ↑(∫ (σ : KSigma 4), sigmaDotRightOntic ctx σ ∂kMuPsi)

§14.2 observable correspondence for I ⊗ σ·b on the singlet.

theorem CSD.LF4.sigmaDotJoint_observable_correspondence (ctx : LF3.MeasurementContext) : LF3.expectation (LF3.sigmaDotJoint ctx.a ctx.b) = ↑(∫ (σ : KSigma 4), sigmaDotJointOntic ctx σ ∂kMuPsi)

§14.2 observable correspondence for σ·a ⊗ σ·b on the singlet. Both sides equal −a·b: the Hilbert side via singlet_pauli_correlation, the ontic side via sigmaDotJointOntic_integral.