LF3/SettingLocality: no-signalling derived from a primitive on Σ

Category: 3-Local (Q10-a / Q10-b).

OperationalNoSignalling.lean's own docstring records the gap this file closes: "sufficient primitive conditions on setting-dependent measure-preserving dynamics over a non-factorising ontic Σ that imply remote marginal invariance remain open". This supplies one, and derives the predicate from it.

The primitive, and why it has this shape

⚠️ The obstruction lives in the readout, not in the measure. That is the Q10-w verdict (specs/q10-no-signalling-scoping.md §4): a factorisation of the typicality measure cannot give remote marginal invariance, because a Fubini argument factorises the integral while the remote setting's dependence sits in the integrand. So a useful primitive must constrain how the remote setting enters the outcome map.

RemoteSettingLocalityA says: changing B's setting from b to b' is implemented by a measure-preserving relabelling of Σ that A's readout cannot see —

• reroute b b' is a measure-preserving self-map of Σ (measurePreserving);
• re-reading A in the moved context at the moved point gives what A read in the old context at the old point (wingA_invariant).

This is the Σ-level, measure-theoretic analogue of the corpus's existing derivation CV.composite_no_signalling, whose primitive is disjoint mode support and whose statement is pointwise on the arena. The scoping doc's candidate (b) — "the setting change acts by a measure-preserving map supported away from the remote readout" — is exactly this.

★ Why this escapes the no_product_partition no-go

LF6.no_product_partition_realises_singlet kills any pair of setting-local response functions: IsProductPartition takes RA RB : DetectorSetting → SigmaSpace → ℝ, so the product structure is the map's arity — there is no slot for the remote setting. That is what sinks the pointwise primitive F_A(a,b,x) = F_A(a,b',x), and it is why Q10's route (a) died.

⚠️ RemoteSettingLocalityA does NOT impose that. S.wingA ⟨a, b⟩ still genuinely depends on b; the hypothesis only says that dependence is carried by a measure-preserving relabelling. So the outcome maps are not forced into product-partition form, the no-go does not apply, and translationLocality below exhibits a witness whose readout really does move with the remote setting while the marginal does not.

Honest scope

• Measurement independence is inherited, not removed. The conclusion is stated against one fixed μ across all four contexts, exactly as OperationalNoSignalling is; that fixture is the Bell premise, and this file does not discharge it. It moves the burden from "assume the marginals agree" to "assume the setting acts by a measure-preserving relabelling" — a strictly more primitive, and falsifiable, hypothesis, but a hypothesis.
• This is a sufficient condition, not a characterisation. No claim that CSD's Σ satisfies it; exhibiting a sector that does is the separate, open half of the row.
• The A-wing and B-wing primitives and derivations are both supplied. ⚠️ Corrected 2026-10-11: for a year the only witness was translationLocality, which satisfies the A-wing primitive alone — its fB C.b l ignores a, which is product-partition arity for B — so operationalNoSignalling_of_settingLocality had no model at all. symmTranslationLocalityB now supplies one; see the last section.

References: specs/q10-no-signalling-scoping.md (the wall-check, the retracted §4 conjecture, and candidate (b)); CV/CompositeArena.lean (composite_no_signalling, the pointwise precedent); CV/ModeLocality.lean (SupportedOn, the model imitated rather than imported); LF6/ForcedContextuality.lean (no_product_partition_realises_singlet, the no-go dodged).

The primitive

structure CSD.LF3.RemoteSettingLocalityA {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) (S : SharedContextOutcomeMaps SigmaSpace) : Type u_1

Setting locality for the A-wing. A change of B's setting is implemented by a measure-preserving relabelling of Σ under which A's reading is unchanged.

Note the arity: wingA keeps its full MeasurementContext, so this does not collapse the outcome maps to a product partition.

• reroute : DetectorSetting → DetectorSetting → SigmaSpace → SigmaSpace

  The relabelling implementing the remote setting change b ↦ b'.

• measurePreserving (b b' : DetectorSetting) : MeasureTheory.MeasurePreserving (self.reroute b b') μ μ

  It preserves the typicality measure.

• wingA_invariant (a b b' : DetectorSetting) (l : SigmaSpace) : S.wingA { a := a, b := b' } (self.reroute b b' l) = S.wingA { a := a, b := b } l

  A's reading in the moved context, at the moved point, is A's reading in the old context at the old point.

structure CSD.LF3.RemoteSettingLocalityB {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) (S : SharedContextOutcomeMaps SigmaSpace) : Type u_1

Setting locality for the B-wing, the mirror statement.

• reroute : DetectorSetting → DetectorSetting → SigmaSpace → SigmaSpace

  The relabelling implementing the remote setting change a ↦ a'.

• measurePreserving (a a' : DetectorSetting) : MeasureTheory.MeasurePreserving (self.reroute a a') μ μ

  It preserves the typicality measure.

• wingB_invariant (a a' b : DetectorSetting) (l : SigmaSpace) : S.wingB { a := a', b := b } (self.reroute a a' l) = S.wingB { a := a, b := b } l

  B's reading is unchanged along it.

★ The derivation

theorem CSD.LF3.remoteMarginalInvariantA_of_settingLocality {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] {μ : MeasureTheory.Measure SigmaSpace} {S : SharedContextOutcomeMaps SigmaSpace} (hS : MeasurableSharedContextOutcomeMaps S) (H : RemoteSettingLocalityA μ S) : RemoteMarginalInvariantA μ S

★ A-wing remote marginal invariance, derived. The proof is one line of measure theory: the moved outcome set is the reroute-preimage of the unmoved one, and reroute preserves μ.

No product structure on Σ, no factorisation of the measure, and no setting-locality of the response functions is used.

theorem CSD.LF3.remoteMarginalInvariantB_of_settingLocality {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] {μ : MeasureTheory.Measure SigmaSpace} {S : SharedContextOutcomeMaps SigmaSpace} (hS : MeasurableSharedContextOutcomeMaps S) (H : RemoteSettingLocalityB μ S) : RemoteMarginalInvariantB μ S

★ B-wing remote marginal invariance, derived — the mirror.

theorem CSD.LF3.operationalNoSignalling_of_settingLocality {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] {μ : MeasureTheory.Measure SigmaSpace} {S : SharedContextOutcomeMaps SigmaSpace} (hS : MeasurableSharedContextOutcomeMaps S) (HA : RemoteSettingLocalityA μ S) (HB : RemoteSettingLocalityB μ S) : OperationalNoSignalling μ S

★★ Operational no-signalling, derived from primitives on Σ. Both wings' setting locality gives the full predicate — the deliverable Q10 was opened for.

★ Non-vacuity: a witness whose readout really does move with the remote setting

Without this the primitive would be worthless: a hypothesis satisfied only by response-independent readouts is the pointwise primitive in disguise, and would be killed by no_product_partition_realises_singlet exactly as route (a) was.

def CSD.LF3.translationMaps {G : Type u_2} [AddGroup G] (fA fB : DetectorSetting → G → Sign) (g : DetectorSetting → G) : SharedContextOutcomeMaps G

The translation model: Σ an additive group, A reading a setting-dependent offset of the ontic point. A's readout genuinely depends on B's setting b, through g b.

Equations

• CSD.LF3.translationMaps fA fB g = { F := fun (C : CSD.LF3.MeasurementContext) (l : G) => (fA C.a (l - g C.b), fB C.b l) }

def CSD.LF3.translationLocality {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (fA fB : DetectorSetting → G → Sign) (g : DetectorSetting → G) : RemoteSettingLocalityA μ (translationMaps fA fB g)

★ The translation model satisfies the primitive. Changing b ↦ b' is implemented by the translation l ↦ l + (g b' - g b), which preserves a translation-invariant μ.

Equations

• CSD.LF3.translationLocality μ fA fB g = { reroute := fun (b b' : CSD.LF3.DetectorSetting) (l : G) => l + (-g b + g b'), measurePreserving := ⋯, wingA_invariant := ⋯ }

theorem CSD.LF3.translation_wingA_setting_dependent {G : Type u_2} [AddGroup G] (fA fB : DetectorSetting → G → Sign) (g : DetectorSetting → G) {a b b' : DetectorSetting} {l : G} (h : fA a (l - g b) ≠ fA a (l - g b')) : (translationMaps fA fB g).wingA { a := a, b := b } l ≠ (translationMaps fA fB g).wingA { a := a, b := b' } l

★ The witness is not response-independent. Whenever the two offsets give A a different reading, wingA genuinely moves with the remote setting — so these outcome maps are not of product-partition arity, and no_product_partition_realises_singlet does not apply to them.

This is what makes the primitive a real weakening rather than a restatement.

★ The symmetric witness: the B-wing primitive gets a model

⚠️ Until 2026-10-11 the B-wing primitive had no witness anywhere in the corpus, so operationalNoSignalling_of_settingLocality — which consumes both — had no model at all. translationLocality supplies the A-wing only, and in translationMaps the B-reading fB C.b l ignores a entirely, which is product-partition arity for B: no_product_partition_realises_singlet applies to that wing, so it cannot be the half of a singlet model. The audit of BACKLOG #131 (specs/two-wing-experiment-scoping.md §4) recorded this as the one place the corpus was emptier than its headline.

The fix is to let each wing see the remote setting through its own offset. The two primitives constrain different wings, so their relabellings are independent and both hold at once.

def CSD.LF3.symmTranslationMaps {G : Type u_2} [AddGroup G] (fA fB : DetectorSetting → G → Sign) (g h : DetectorSetting → G) : SharedContextOutcomeMaps G

The symmetric translation model: each wing reads a remotely offset ontic point — A through g C.b and B through h C.a. Compare translationMaps, whose B-reading ignores a.

Equations

• CSD.LF3.symmTranslationMaps fA fB g h = { F := fun (C : CSD.LF3.MeasurementContext) (l : G) => (fA C.a (l - g C.b), fB C.b (l - h C.a)) }

theorem CSD.LF3.measurable_symmTranslationMaps {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] {fA fB : DetectorSetting → G → Sign} (hfA : ∀ (a : DetectorSetting), Measurable (fA a)) (hfB : ∀ (b : DetectorSetting), Measurable (fB b)) (g h : DetectorSetting → G) : MeasurableSharedContextOutcomeMaps (symmTranslationMaps fA fB g h)

The symmetric model's outcome maps are measurable, given measurable wing responses.

def CSD.LF3.symmTranslationLocalityA {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (fA fB : DetectorSetting → G → Sign) (g h : DetectorSetting → G) : RemoteSettingLocalityA μ (symmTranslationMaps fA fB g h)

★ The symmetric model satisfies the A-wing primitive, exactly as translationLocality does: the extra h C.a in the B-reading is invisible to wingA.

Equations

• CSD.LF3.symmTranslationLocalityA μ fA fB g h = { reroute := fun (b b' : CSD.LF3.DetectorSetting) (l : G) => l + (-g b + g b'), measurePreserving := ⋯, wingA_invariant := ⋯ }

def CSD.LF3.symmTranslationLocalityB {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (fA fB : DetectorSetting → G → Sign) (g h : DetectorSetting → G) : RemoteSettingLocalityB μ (symmTranslationMaps fA fB g h)

★★★ The B-wing primitive gets its witness. The mirror relabelling l ↦ l + (-h a + h a') leaves B's reading unchanged, because B sees A's setting only through the offset h a. This is the declaration whose absence left operationalNoSignalling_of_settingLocality without a model.

Equations

• CSD.LF3.symmTranslationLocalityB μ fA fB g h = { reroute := fun (a a' : CSD.LF3.DetectorSetting) (l : G) => l + (-h a + h a'), measurePreserving := ⋯, wingB_invariant := ⋯ }

theorem CSD.LF3.operationalNoSignalling_symmTranslation {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] {fA fB : DetectorSetting → G → Sign} (hfA : ∀ (a : DetectorSetting), Measurable (fA a)) (hfB : ∀ (b : DetectorSetting), Measurable (fB b)) (g h : DetectorSetting → G) : OperationalNoSignalling μ (symmTranslationMaps fA fB g h)

★★★ operationalNoSignalling_of_settingLocality now has a model. Both primitives hold of the symmetric translation model, so the derived predicate is inhabited and the theorem is not vacuous.

⚠️ What this does not say: that the model reproduces P_st. It is a witness for the primitives, and the content of the witness is that neither wing is of product-partition arity (the two lemmas below), so no_product_partition_realises_singlet does not apply to it. Whether some instance of this shape realises the singlet's correlations is a further question and is not settled here.

theorem CSD.LF3.symmTranslation_wingA_setting_dependent {G : Type u_2} [AddGroup G] (fA fB : DetectorSetting → G → Sign) (g h : DetectorSetting → G) {a b b' : DetectorSetting} {l : G} (hne : fA a (l - g b) ≠ fA a (l - g b')) : (symmTranslationMaps fA fB g h).wingA { a := a, b := b } l ≠ (symmTranslationMaps fA fB g h).wingA { a := a, b := b' } l

★ A's reading moves with the remote setting in the symmetric model.

theorem CSD.LF3.symmTranslation_wingB_setting_dependent {G : Type u_2} [AddGroup G] (fA fB : DetectorSetting → G → Sign) (g h : DetectorSetting → G) {a a' b : DetectorSetting} {l : G} (hne : fB b (l - h a) ≠ fB b (l - h a')) : (symmTranslationMaps fA fB g h).wingB { a := a, b := b } l ≠ (symmTranslationMaps fA fB g h).wingB { a := a', b := b } l

★ And so does B's — which translationMaps could not manage. This is what makes the B-wing witness a real one: wingB genuinely depends on the remote setting a, so these outcome maps are not of product-partition arity and the no-go does not reach them.