LF3 ContextMap: measurement contexts and the Bell-consistency boundary

Category: 3-Local (LF3 context-indexed outcome maps and the Bell-consistency interface; the no-go is proved downstream on a shared domain, LF6.no_compatible_global_chsh_assignment_realises_singlet).

Paper §8 / §9.9.

ContextMap records the distinction between context-indexed realised outcomes and a setting-local global CHSH assignment. Type separation alone does NOT prove incompatibility — different structures establish only definitional separation. The mathematical obstruction is supplied downstream by the CHSH theorem and LF6.no_product_partition_realises_singlet, and on one shared state space by LF6.no_compatible_global_chsh_assignment_realises_singlet.

Six context theorems re-state Singlet/Kernel results in MeasurementContext form for the paper's §8.12 export list.

structure CSD.LF3.MeasurementContext : Type

A measurement context: a choice of detector settings on the two wings.

• a : DetectorSetting

  A-wing detector setting.

• b : DetectorSetting

  B-wing detector setting.

structure CSD.LF3.ContextIndexedOutcomeMaps : Type (u_1 + 1)

Context-indexed outcome maps. Each context has its own per-context state space Domain ctx, and each state x : Domain ctx is assigned a joint outcome (s, t) : Sign × Sign. In the full ontic interpretation Domain ctx would be a Σ-basin family; at the LF3 Lean level it stays abstract.

• Domain : MeasurementContext → Type u_1

  The per-context state space.

• F (ctx : MeasurementContext) : self.Domain ctx → Sign × Sign

  The outcome map.

structure CSD.LF3.GlobalCHSHAssignment (HiddenState : Type u_1) : Type u_1

A global CHSH assignment: a single map from one hidden-state space to simultaneous outcomes for all four Bell-test settings (paper §8.7). This is not the same data type as ContextIndexedOutcomeMaps — different fields, different domains. ⚠️ Type separation alone does NOT prove incompatibility; the earlier claim that it "carries the Bell-consistency content" was false. Different structures give definitional separation and nothing more.

Worse, the separation did not merely fail to prove the no-go — it prevented the no-go from being stated, because ContextIndexedOutcomeMaps gives each context its own Domain ctx, so there is nothing to compare against a global assignment on one state space. The obstruction becomes expressible only on a shared domain (LF3.SharedContextOutcomeMaps), and is proved there by LF6.no_compatible_global_chsh_assignment_realises_singlet.

• A1 : HiddenState → Sign

  A-wing outcome for setting 1.

• A2 : HiddenState → Sign

  A-wing outcome for setting 2.

• B1 : HiddenState → Sign

  B-wing outcome for setting 1.

• B2 : HiddenState → Sign

  B-wing outcome for setting 2.

Context theorem targets (paper §8.12 / spec §9.9)

theorem CSD.LF3.context_singlet_kernel (ctx : MeasurementContext) (s t : Sign) : P_st ctx.a ctx.b s t = (1 - s.val * t.val * dotR ctx.a ctx.b) / 4

The pointer-sector kernel at a measurement context (paper §8.12).

theorem CSD.LF3.context_correlation_eq_neg_dot (ctx : MeasurementContext) : ∑ st : Sign × Sign, st.1.val * st.2.val * P_st ctx.a ctx.b st.1 st.2 = -dotR ctx.a ctx.b

The Bell correlation at a measurement context (paper §8.12).

theorem CSD.LF3.context_marginal_a (ctx : MeasurementContext) (s : Sign) : ∑ t : Sign, P_st ctx.a ctx.b s t = 1 / 2

The A-side marginal at a measurement context (paper §8.12).

theorem CSD.LF3.context_marginal_b (ctx : MeasurementContext) (t : Sign) : ∑ s : Sign, P_st ctx.a ctx.b s t = 1 / 2

The B-side marginal at a measurement context.

theorem CSD.LF3.context_no_signalling_a (ctx : MeasurementContext) (b' : DetectorSetting) (s : Sign) : ∑ t : Sign, P_st ctx.a ctx.b s t = ∑ t : Sign, P_st ctx.a b' s t

A-side no-signalling at a measurement context (paper §8.12).

theorem CSD.LF3.context_no_signalling_b (ctx : MeasurementContext) (a' : DetectorSetting) (t : Sign) : ∑ s : Sign, P_st ctx.a ctx.b s t = ∑ s : Sign, P_st a' ctx.b s t

B-side no-signalling at a measurement context.