LF3/SettingLocalityLocal: the setting-locality primitive, aware of the local setting

Category: 3-Local (Q10-a / Q10-b; BACKLOG #137).

SettingLocality.lean's primitives let a change of the remote setting be implemented by a measure-preserving relabelling of Σ — reroute b b' for the A-wing, reroute a a' for the B-wing — and the relabelling there is blind to the local setting: one map reroute a a' has to leave wingB ⟨a, b⟩ invariant for every b at once.

That blindness is stronger than the derivation needs, and #137 found it is too strong to be satisfied at the record-layer basins. The derivation (remoteMarginalInvariantB_of_settingLocality) uses, for each fixed b, only the map at that b; nothing couples different b. But a b-blind map forces the counterfactual joint law of B's two readings under b and b', μ {l | wingB ⟨a, b⟩ l = t ∧ wingB ⟨a, b'⟩ l = t'}, to be independent of a — it is the measure of an intersection the relabelling carries to the corresponding intersection at a'. At the I3 record basins (RecordLayer/SkewFibrePartition.lean) that joint law is ∑ₛ rowSum s · |B-arc(s,t;a,b) ∩ B-arc(s,t';a,b')|, and for the singlet at the CHSH angles it takes the values (1 − √2/2)/2 at one a and 1/2 at the other: no b-blind B-reroute exists for the singlet tables in the I3 geometry (and, by the Fréchet bounds on the within-cell overlaps, in any geometry whose A-cells are shared across b). Formalising that obstruction is a priced row; what this file does is state the primitive the derivation actually consumes.

• LocalSettingLocalityA μ S / LocalSettingLocalityB μ S: the relabelling may depend on the local setting too — reroute a b b' for the A-wing (a local), reroute a a' b for the B-wing (b local). Everything else is as before: measure-preserving, local reading invariant.
• RemoteSettingLocalityA.toLocal / B.toLocal: the blind primitive is the special case.
• ★ remoteMarginalInvariantA_of_localSettingLocality, ★ …B_…, ★★ operationalNoSignalling_of_localSettingLocality: the same derivation goes through — one line of measure theory per wing, with the local setting fixed throughout.

Honest scope

• Exactly as for the blind primitive: measurement independence (one μ for all contexts) is inherited, not removed; this is a sufficient condition, not a characterisation; and the response maps are not forced into product-partition arity, so LF6.no_product_partition_realises_singlet does not reach them.
• The witness that CSD's record-layer basins satisfy LocalSettingLocalityB is RecordLayer/SkewReroute.lean (#137).

References: SettingLocality.lean (RemoteSettingLocalityA/B, the derivations imitated); RecordLayer/SkewFibrePartition.lean (eq_of_vadd_preimage_circleCell_eq, the first no-go on the reroute's shape); specs/BACKLOG.md #137, #131 obligation (4).

The local-setting-aware primitive

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

Setting locality for the A-wing, aware of A's own setting. A change of B's setting b ↦ b' is implemented, at each a, by a measure-preserving relabelling of Σ under which A's reading in context ⟨a, ·⟩ is unchanged.

• reroute : DetectorSetting → DetectorSetting → DetectorSetting → SigmaSpace → SigmaSpace

  The relabelling implementing b ↦ b', at A's setting a.

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

  It preserves the typicality measure.

• wingA_invariant (a b b' : DetectorSetting) (l : SigmaSpace) : S.wingA { a := a, b := b' } (self.reroute a 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.

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

Setting locality for the B-wing, aware of B's own setting — the mirror.

• reroute : DetectorSetting → DetectorSetting → DetectorSetting → SigmaSpace → SigmaSpace

  The relabelling implementing a ↦ a', at B's setting b.

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

  It preserves the typicality measure.

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

  B's reading is unchanged along it.

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

The blind A-primitive is the special case whose relabelling ignores a.

Equations

• H.toLocal = { reroute := fun (x b b' : CSD.LF3.DetectorSetting) => H.reroute b b', measurePreserving := ⋯, wingA_invariant := ⋯ }

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

The blind B-primitive is the special case whose relabelling ignores b.

Equations

• H.toLocal = { reroute := fun (a a' x : CSD.LF3.DetectorSetting) => H.reroute a a', measurePreserving := ⋯, wingB_invariant := ⋯ }

★ The derivation, unchanged

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

★ A-wing remote marginal invariance from the local-setting-aware primitive. The proof is the one of remoteMarginalInvariantA_of_settingLocality with a fixed throughout.

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

★ B-wing remote marginal invariance from the local-setting-aware primitive — the mirror.

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

★★ Operational no-signalling from the local-setting-aware primitives on both wings.