LF3/OperationalNoSignalling: remote marginal invariance, at the measure level

Category: 3-Local (the operational no-signalling predicate).

Why this is stated at the measure level

The tempting formulation is pointwise: F_A(a, b, x) = F_A(a, b', x) for every x, and symmetrically for B. That is not merely too strong — over a deterministic shared state it is inconsistent with the rest of the programme. Setting A(a,x) := F_A(a, b₀, x) and B(b,x) := F_B(a₀, b, x) recovers exactly the setting-local response pair that LF6.no_product_partition_realises_singlet rules out for the singlet. An assumption that is false in the sector under discussion is worse than a missing one.

So the correct operational condition is equality of marginal measures under a remote setting change, never equality of the underlying outcome regions.

⚠️ What this rests on: measurement independence

OperationalNoSignalling is stated relative to one fixed μ, used for all four contexts. That fixture is measurement independence (the assumption that the ontic distribution does not depend on which settings are chosen). It is a genuine Bell premise, and naming it here is deliberate: it was previously invisible, carried silently by the shape of the definition rather than stated.

Anything downstream that appeals to these predicates is therefore assuming measurement independence, and should say so.

⚠️ What this is not

Verifying this predicate in a constructed sector is not a derivation of no-signalling from primitives. ★ A sufficient primitive condition now exists (LF3/SettingLocality.lean, 2026-09-01): if a remote setting change is implemented by a measure-preserving relabelling of Σ along which the local wing's reading is unchanged, remote marginal invariance follows (operationalNoSignalling_of_settingLocality). ⚠️ That is a sufficient condition, not a characterisation, and it does not discharge the measurement-independence fixture above — it inherits it. Whether CSD's own Σ satisfies it is the open half.

References

LF3/SharedContextMap.lean; LF3/ContextMap.lean (context_no_signalling_a/b); LF6/ForcedContextuality.lean; specs/c1-correction-plan.md §1.

def CSD.LF3.RemoteMarginalInvariantA {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) (S : SharedContextOutcomeMaps SigmaSpace) : Prop

A-wing remote marginal invariance. The measure of the event "A reads s" is unchanged when B's setting moves from b to b'.

Equality of measures, not of the underlying outcome sets: the microscopic region realising "A reads s" may differ entirely between the two contexts.

Equations

• One or more equations did not get rendered due to their size.

def CSD.LF3.RemoteMarginalInvariantB {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) (S : SharedContextOutcomeMaps SigmaSpace) : Prop

B-wing remote marginal invariance, symmetrically.

Equations

• One or more equations did not get rendered due to their size.

def CSD.LF3.OperationalNoSignalling {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) (S : SharedContextOutcomeMaps SigmaSpace) : Prop

Operational no-signalling: both wings' marginals are invariant under a remote setting change.

⚠️ Stated relative to a single fixed μ across all four contexts. That fixture is measurement independence, and it is a premise, not a consequence.

Equations

• CSD.LF3.OperationalNoSignalling μ S = (CSD.LF3.RemoteMarginalInvariantA μ S ∧ CSD.LF3.RemoteMarginalInvariantB μ S)

The singlet kernel is operationally no-signalling

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

★ The singlet kernel satisfies remote marginal invariance on both wings, in one statement.

This is the kernel-level fact, assembled from the machine-checked context_no_signalling_a and context_no_signalling_b. It is a verification in the constructed sector, not a derivation from primitives.

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

Both wings' marginals are 1/2 at every context: the singlet is locally maximally mixed, which is the strongest form of "the remote setting is invisible".