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 is done in full and the B-wing is its mirror; both are supplied.

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.