LF3/SharedContextMap: outcome maps on ONE shared state space #

Category: 3-Local (the shared-domain context interface).

ContextIndexedOutcomeMaps gives each context its own state space Domain ctx. That is the wrong shape for the C1 Bell analysis, which fixes a single ontic state space SigmaSpace and asks what a family of context-indexed outcome maps on it can do. This module supplies that shape.

SharedContextOutcomeMaps SigmaSpace — one common SigmaSpace, an outcome map per context. The state type does not depend on the context.
MeasurableSharedContextOutcomeMaps — each F C : SigmaSpace → Sign × Sign is measurable. This is the only measurability assumed anywhere in the C1 chain: the four setting-local responses of a GlobalCHSHAssignment are derived measurable from it and compatibility, never assumed. See LF6/C1BellConsistency.lean.

Sign carries the discrete (⊤) σ-algebra, the canonical choice for a finite type and the one that makes "measurable outcome map" mean what it should.

Notation bridge. The type variable SigmaSpace is named for the intended CSD instantiation (the ontic surface Σ), but it is Bell's Λ — an arbitrary shared state space, nothing CSD-specific. The general theorems built on this interface owe their transfer-to-rivals force to exactly that generality; the QM-side E91.lean keeps Bell's Λ spelling because it is literature-facing. One object, two communities' names.

References #

LF3/ContextMap.lean (MeasurementContext, GlobalCHSHAssignment); LF6/C1BellConsistency.lean (the no-go this feeds); specs/c1-correction-plan.md §3 D1.

source

@[instance_reducible]

instance CSD.LF3.instMeasurableSpaceSign :

MeasurableSpace Sign

The discrete σ-algebra on Sign: every subset is measurable.

Equations

CSD.LF3.instMeasurableSpaceSign = ⊤

source

instance CSD.LF3.instMeasurableSingletonClassSign :

MeasurableSingletonClass Sign

Singletons are measurable in the discrete σ-algebra — the companion instance the level-set arguments of LF6/C1BellConsistency.lean consume.

source

theorem CSD.LF3.measurable_of_sign {α : Type u_1} [MeasurableSpace α] (f : Sign → α) :

Measurable f

Every function out of Sign is measurable, Sign being discrete.

source

structure CSD.LF3.SharedContextOutcomeMaps (SigmaSpace : Type u_1) :

Type u_1

Outcome maps on one shared state space. Every context reads the same SigmaSpace; only the outcome map varies. This is the C1 shape: a fixed ontic state space, with the context selecting how it is read.