The two-wing record violates the CHSH bound

Category: 3-Local (the entangled de-isolation tier). BACKLOG #131, obligation (4), the Bell half.

The no-signalling half of obligation (4) landed with LF3.symmTranslationLocalityB (the primitive's missing model) and the marginal theorems of TwoWingRecord.lean. This is the other half, and it is the last item on #131 with a price: the CHSH combination of the two-wing record correlations is −2√2.

What is new here, and what is imported

⚠️ No Bell theorem is proved here, and none is needed. The singlet's E(a, b) = −a·b is LF3.correlation_eq_neg_dot, the −2√2 at the canonical angles is Empirical.Bell.chsh_singlet_at_optimal_angles, and the local-hidden-variable bound |S| ≤ 2 is Empirical.QM.E91.lhvCHSH_abs_le_two over a genuine measure-theoretic model. All three are imported.

What is new is the quantity being correlated. Until now the corpus' CHSH was a function of P_st — an algebraic kernel. Here it is a function of the measures of record events on Σ: sets of ontic microstates, read in epistemicMeasure, after the de-isolation flow from the prepared ray. So for the first time Bell violation is a statement about the same objects as no-signalling (toReal_measure_preimage_wingAEvent_eq_of_setting), record stability (RecordLayer.measure_drift_wingCode_ne_le) and causal separation (CV.spacelike_twoWing) — which is exactly what #131 asked for and what "within the same dynamical model" means.

• recordCorrelation e p — the correlation of the two-wing record events at a ray;
• ★★★ recordCorrelation_eq_correlation and ★★★ recordCorrelation_eq_neg_dotR — it is the singlet correlation, −a·b, at every setting pair and with no genericity hypothesis;
• preparedRecordCorrelation a b — the same read at the prepared, pre-measurement ray, through liftBase localDeisolationFlow, with ★★★ preparedRecordCorrelation_eq_correlation;
• ★★★ chsh_preparedRecord_eq_neg_two_sqrt_two — the CHSH of the four prepared-ray record correlations is −2√2 at the canonical angles;
• ★★★ bellClassicalBound_lt_abs_chsh_preparedRecord — and that exceeds the local-hidden-variable bound: 2 < |S| = 2√2.

Honest scope

⚠️ The four terms are four different runs. Each preparedRecordCorrelation a b is evaluated in its own prepared measure, at the ray preparedRay a b built from localNudgeVec a b. That is what a Bell test is — four setting configurations, separate runs — but it is not the single-μ idealisation LF3.OperationalNoSignalling is stated in. Both are in the corpus and they must not be run together: the no-signalling predicate fixes one measure across contexts (which is the measurement-independence premise), while this statement ranges over four preparations.

⚠️ This does not make CSD local, and does not pretend to. The record events move with the joint context (RecordLayer.wingCode_ne_of_mem_of_mem), so the outcome maps are not of product-partition arity and LF6.no_product_partition_realises_singlet does not apply — which is why a violation is possible at all. Nothing here is a non-contextual value assignment, and the violation is of the LHV bound, not of anything CSD claims.

⚠️ P_st is not re-derived and the angles are not optimised. chshA, chshA', chshB, chshB' are the canonical settings already in Empirical/QM/Bell.lean; nothing here shows they are optimal (that is Tsirelson, chsh_inner_bound, also already there).

⚠️ Still not C-1. Causal adjacency is supplied through CV.twoWingGraph, and nothing here shows that the apparent nonlocality is a consequence of projection alone. #131 says so explicitly, and obligation (4) being discharged does not change it.

References: TwoWingRecord.lean (recordCorrelation's ingredients: pointerDecode, toReal_measure_wingEvent_eq_P_st, toReal_measure_preimage_wingEvent_eq_P_st, preparedRay), NudgeLocality.lean (localNudgeVec), Empirical/QM/Bell.lean (correlation, chshOperator, chsh_singlet_at_optimal_angles, bellClassicalBoundValue, chsh_classical_bound_violated), Empirical/QM/Crypto/E91.lean (lhvCHSH_abs_le_two, the LHV bound this exceeds), LF3/Singlet/Kernel.lean (P_st, dotR); specs/BACKLOG.md #131 obligation (4); specs/two-wing-experiment-scoping.md §6.

The correlation of the record events

noncomputable def CSD.LF6.recordCorrelation {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (p : LF4.CPN (M + 1)) : ℝ

The two-wing record correlation at a ray: the ±1-weighted sum of the Born weights of the joint record events. The quantity a Bell test measures, with the outcomes read off Σ rather than off an algebraic kernel.

Equations

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

theorem CSD.LF6.recordCorrelation_eq_correlation {M : ℕ} (a b : LF3.DetectorSetting) (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin localDeisolationV) (localNudgeVec a b))) (hψ'0 : ψ' ≠ 0) : recordCorrelation e (Projectivization.mk ℂ ψ' hψ'0) = Empirical.Bell.correlation a b

★★★ The record correlation is the singlet correlation. Term by term, by toReal_measure_wingEvent_eq_P_st: the measure of the record event for (s, t) is P_st a b s t, so the sum is the kernel's own correlation. No genericity hypothesis.

theorem CSD.LF6.recordCorrelation_eq_neg_dotR {M : ℕ} (a b : LF3.DetectorSetting) (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin localDeisolationV) (localNudgeVec a b))) (hψ'0 : ψ' ≠ 0) : recordCorrelation e (Projectivization.mk ℂ ψ' hψ'0) = -LF3.dotR a b

★★★ Hence −a·b, the singlet's closed form, now as a statement about the measures of record events.

Read at the prepared ray, along the flow

noncomputable def CSD.LF6.preparedRecordCorrelation (a b : LF3.DetectorSetting) : ℝ

The two-wing record correlation of a run: the same ±1-weighted sum, but in the prepared, pre-measurement epistemic measure, with the record events pulled back along the lifted de-isolation flow. This is the correlation of an actual run of the experiment.

Equations

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

theorem CSD.LF6.preparedRecordCorrelation_eq_correlation (a b : LF3.DetectorSetting) : preparedRecordCorrelation a b = Empirical.Bell.correlation a b

★★★ The run's record correlation is the singlet correlation. Everything about the dynamics is already in toReal_measure_preimage_wingEvent_eq_P_st; this is that theorem summed against the ±1 weights.

theorem CSD.LF6.preparedRecordCorrelation_eq_neg_dotR (a b : LF3.DetectorSetting) : preparedRecordCorrelation a b = -LF3.dotR a b

The CHSH violation

noncomputable def CSD.LF6.chshPreparedRecord : ℝ

The CHSH combination of the four runs' record correlations. Four setting configurations, four prepared rays, four flows — as in an actual Bell test.

Equations

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

theorem CSD.LF6.chshPreparedRecord_eq_chshOperator : chshPreparedRecord = Empirical.Bell.chshOperator Empirical.Bell.chshA Empirical.Bell.chshA' Empirical.Bell.chshB Empirical.Bell.chshB'

The record CHSH is the kernel's CHSH, term by term.

theorem CSD.LF6.chsh_preparedRecord_eq_neg_two_sqrt_two : chshPreparedRecord = -(2 * √2)

★★★ The two-wing record's CHSH value is −2√2. The correlated quantities are measures of record events on Σ, in the prepared epistemic measure, after the de-isolation flow — so this is the Bell half of #131 obligation (4): the same model that carries no-signalling, record stability and causal separation also violates CHSH.

theorem CSD.LF6.bellClassicalBound_lt_abs_chsh_preparedRecord : Empirical.Bell.bellClassicalBoundValue < |chshPreparedRecord|

★★★ And it exceeds the local-hidden-variable bound. 2 < 2√2, with the bound itself proved over a genuine measure-theoretic hidden-variable model in Empirical.QM.E91.lhvCHSH_abs_le_two — so no such model reproduces this record's statistics.