The blind B-wing primitive is unsatisfiable at the I3 record basins for the singlet

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #156 (out of #137): the finding, as a theorem.

LF3.RemoteSettingLocalityB asks for one relabelling reroute a a' that carries B's reading in context ⟨a, b⟩ to its reading in ⟨a', b⟩ for every b. #137 observed that this is more than the derivation uses and that the record layer cannot supply it. This file proves the second half.

• ★ LF3.measure_counterfactual_eq_of_remoteSettingLocalityB: a blind reroute equates the counterfactual joint laws — μ {l | wingB ⟨a,b⟩ l = t ∧ wingB ⟨a,b'⟩ l = t'} is the same at a and at a', because the one relabelling carries the intersection at a' back to the intersection at a, and it preserves μ. Pure measure theory, any Σ.
• counterfactual_eq_iUnion, ★ volume_counterfactual: at the I3 skew cells of two tables with the same A-marginal, the counterfactual set is ⋃ₛ A_s × (B_{s,t} ∩ B'_{s,t'}), with measure ∑ₛ |A_s| · |B_{s,t} ∩ B'_{s,t'}|.
• ★★ volume_counterfactual_singlet: for the singlet, vol {wingB ⟨a,b⟩ = + ∧ wingB ⟨a,b'⟩ = +} = ½ min((1−d)/2, (1−d')/2) + ½ min((1+d)/2, (1+d')/2) with d = a·b, d' = a·b' (cfJoint).
• ★★★ not_nonempty_remoteSettingLocalityB_singlet: no blind B-reroute exists for the singlet on the I3 record basins. At the circle settings a = 0, a' = π/2, b = π/4, b' = −π/4 the counterfactual law is 1/2 at a and (1 − √2/2)/2 at a'; √2 ≠ 0.

What this says

The record layer satisfies the primitive the derivation consumes (LocalSettingLocalityB, SkewReroute.lean, SingletSkewTables.lean) and cannot satisfy the blind one. The obstruction is not a feature of the rectangle exchange but of any b-blind map whatsoever: the counterfactual joint law of B's two readings is an invariant of such a map, and the singlet's tables make it depend on a. A sharper reading: the blind primitive would force a joint distribution of B's counterfactual readings under two settings that is independent of A's setting, which Bell-violating tables refuse.

Honest scope

• The obstruction is stated at the I3 skew cells with A's cells shared across b (the geometry the record layer has). The paragraph in SettingLocalityLocal.lean argues the same for any geometry with shared A-cells via the Fréchet bounds; that generalisation is not formalised.
• Four specific circle settings; the general contrast criterion (|a·b − a·b'| ≠ |a'·b − a'·b'|) is visible in cfJoint but stated only through this instance.

References: LF3/SettingLocality.lean (RemoteSettingLocalityB), LF3/SettingLocalityLocal.lean (the restated primitive and the prose argument), SkewReroute.lean (skewIdx, skewOutcomeMaps), SingletSkewTables.lean (singletTables), Empirical/QM/ColbeckRenner.lean (circleSetting, dotR_circleSetting); specs/BACKLOG.md #156, #137.

theorem CSD.LF3.measure_counterfactual_eq_of_remoteSettingLocalityB {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] {μ : MeasureTheory.Measure SigmaSpace} {S : SharedContextOutcomeMaps SigmaSpace} (hS : MeasurableSharedContextOutcomeMaps S) (H : RemoteSettingLocalityB μ S) (a a' b b' : DetectorSetting) (t t' : Sign) : μ {l : SigmaSpace | S.wingB { a := a, b := b } l = t ∧ S.wingB { a := a, b := b' } l = t'} = μ {l : SigmaSpace | S.wingB { a := a', b := b } l = t ∧ S.wingB { a := a', b := b' } l = t'}

★ A blind B-reroute equates the counterfactual joint laws of B's two readings at a and at a': the one relabelling carries the intersection at a' back to the intersection at a.

The counterfactual set at the skew cells

theorem CSD.RecordLayer.counterfactual_eq_iUnion {m n : ℕ} {q q' : JointRates m n} (hrow : q.rowSum = q'.rowSum) (t t' : Fin n) : {θ : LF4.KTorus | (skewIdx q θ).2 = t ∧ (skewIdx q' θ).2 = t'} = ⋃ (s : Fin m), circleCell q.rowSum s ×ˢ (circleCell (q.condRate s) t ∩ circleCell (q'.condRate s) t')

With the same A-marginal, the counterfactual set is a union over A's cells of rectangles.

theorem CSD.RecordLayer.volume_counterfactual {m n : ℕ} {q q' : JointRates m n} (hrow : q.rowSum = q'.rowSum) (t t' : Fin n) : MeasureTheory.volume {θ : LF4.KTorus | (skewIdx q θ).2 = t ∧ (skewIdx q' θ).2 = t'} = ∑ s : Fin m, MeasureTheory.volume (circleCell q.rowSum s) * MeasureTheory.volume (circleCell (q.condRate s) t ∩ circleCell (q'.condRate s) t')

★ The counterfactual law at the skew cells: ∑ₛ |A_s| · |B_{s,t} ∩ B'_{s,t'}|.

The singlet's counterfactual law

noncomputable def CSD.RecordLayer.cfJoint (d d' : ℝ) : ℝ

The counterfactual joint law of B's + readings under b and b', as a function of the two correlations d = a·b, d' = a·b'.

Equations

• CSD.RecordLayer.cfJoint d d' = 1 / 2 * min ((1 - d) / 2) ((1 - d') / 2) + 1 / 2 * min ((1 + d) / 2) ((1 + d') / 2)

theorem CSD.RecordLayer.signOfFin_eq_plus_iff (x : Fin 2) : signOfFin x = LF3.Sign.plus ↔ x = 0

theorem CSD.RecordLayer.singletJointRates_condRate_zero (a b : LF3.DetectorSetting) (s : Fin 2) : (singletJointRates a b).condRate s 0 = 2 * LF3.P_st a b (signOfFin s) LF3.Sign.plus

The conditional probability of B's + given A's s, for the singlet.

theorem CSD.RecordLayer.circleCell_condRate_zero_inter {m n : ℕ} [NeZero n] (q q' : JointRates m n) (s : Fin m) : circleCell (q.condRate s) 0 ∩ circleCell (q'.condRate s) 0 = rep ⁻¹' Set.Ioc 0 (min (q.condRate s 0) (q'.condRate s 0))

Two initial arcs intersect in the initial arc of the smaller length.

theorem CSD.RecordLayer.volume_counterfactual_singlet (a b b' : LF3.DetectorSetting) : MeasureTheory.volume {θ : LF4.KTorus | (skewOutcomeMaps singletTables).wingB { a := a, b := b } θ = LF3.Sign.plus ∧ (skewOutcomeMaps singletTables).wingB { a := a, b := b' } θ = LF3.Sign.plus} = ENNReal.ofReal (cfJoint (LF3.dotR a b) (LF3.dotR a b'))

★★ The singlet's counterfactual law of B's + readings under b and b', at the I3 skew cells.

★★★ The obstruction

theorem CSD.RecordLayer.not_nonempty_remoteSettingLocalityB_singlet : ¬Nonempty (LF3.RemoteSettingLocalityB MeasureTheory.volume (skewOutcomeMaps singletTables))

★★★ No blind B-wing reroute exists for the singlet on the I3 record basins. A blind reroute would equate the counterfactual joint laws at a = 0 and a' = π/2 (settings on the great circle, with b = π/4, b' = −π/4); they are 1/2 and (1 − √2/2)/2.