The setting-locality primitive at the I3 record basins: the skew rectangle exchange

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #137 (out of #131 obligation (4)): the instantiation the audit asked for.

The choice, in one paragraph

I3, and the reroute is a rectangle exchange. Under I3 the fibre T² is tiled exactly by the skew cells skewCell q s t = A_s × B_{s,t} of the joint context's table q (existsUnique_mem_skewCell); A reads the θ₁-cell, B the θ₂-cell conditional on A's. A change of B's setting leaves A's cells alone when the tables are no-signalling (rowSum independent of b), so A's reroute is the identity (wingA_eq_of_rowSum_eq). For B, a change of A's setting a ↦ a' replaces the table q = Q⟨a, b⟩ by q' = Q⟨a', b⟩, and B's region for the outcome t, ⋃ₛ A_s × B_{s,t}, is a different staircase of the same total height colSum t. The reroute normalises each skew cell A_s × B_{s,t} onto a rectangle N_{s,t} of the horizontal band [0,1) × C_t (C_t the arc of colSum t), by the Jacobian-one affine map that stretches θ₁ by (rate s t / colSum t) / rowSum s and θ₂ by its reciprocal (toNormal, normalize), and then denormalises with the inverse exchange for q' (toSkew, denormalize): reroute q q' = denormalize q' ∘ normalize q. Each half is a glued family of Jacobian-one affine rectangle maps between two exact tilings (GluedMeasurePreserving.lean, ArcAffine.lean), hence measure-preserving (★★ measurePreserving_reroute); the band C_t is the same for q and q' because colSum is, so B's reading is carried along (★★ wingB_reroute). The map is not fibrewise (it moves θ₁ across A's cells), which is exactly what eq_of_vadd_preimage_circleCell_eq said it must do.

What is proved

• existsUnique_mem_skewCell, existsUnique_mem_normalCell: the skew cells and the normal cells are exact tilings of the fibre; skewIdx / normalIdx read the cell of a point.
• toNormal, toSkew: the Jacobian-one affine maps between a skew cell and its normal cell, and back; toNormal_mem, toSkew_mem (pointwise), ★ map_restrict_toNormal, ★ map_restrict_toSkew (the measure transport, exact).
• normalize, denormalize: the glued exchanges; ★★ measurePreserving_normalize, ★★ measurePreserving_denormalize.
• reroute q q': ★★ measurePreserving_reroute, ★★ wingB_reroute (needs q.colSum = q'.colSum); wingA_eq_of_rowSum_eq.
• The LF3 instance, for a family of 2 × 2 tables Q : MeasurementContext → JointRates 2 2: skewOutcomeMaps Q (A reads the θ₁-cell, B the conditional θ₂-cell, as signs), measurable_skewOutcomeMaps; ★★★ skewLocalSettingLocalityA (identity reroute, needs A's marginal independent of b), ★★★ skewLocalSettingLocalityB (the rectangle exchange, needs B's marginal independent of a); ★★★ operationalNoSignalling_skew: operational no-signalling for the I3 record basins, derived from the primitive — not assumed from the tables' marginals, although it needs them to agree, which is what makes the primitive instantiable at all.

⚠️ The finding: the blind primitive is unsatisfiable here

LF3.RemoteSettingLocalityB wants one reroute a a' for all b. The exchange above depends on b through Q⟨a, b⟩, and no b-blind map can replace it for Bell-violating tables: a b-blind map carries R_t(a,b) ∩ R_{t'}(a,b') onto R_t(a',b) ∩ R_{t'}(a',b'), so the counterfactual joint law of B's two readings would have to be independent of a, and for the singlet at the CHSH settings it is not (the computation is in LF3/SettingLocalityLocal.lean). What the record layer satisfies is the local-setting-aware primitive LocalSettingLocalityB, which derives the same no-signalling. Formalising the obstruction is a priced row.

Honest scope

• The fibre, with the tables as data. Σ = T² here with Haar measure; the base-coupled version (SkewBasin.lean's skewBasin over KSigma N, with epistemicMeasure p = δ_p ⊗ vol) is the same construction fibrewise over the base point and is priced as the continuation.
• No-signalling of the tables is a hypothesis on Q (rowSum independent of b, colSum of a). It is what the Born tables of any joint context satisfy, and it is necessary for the primitive (the readings' marginals must agree); nothing here derives it from dynamics.
• 2 × 2 outcomes in the LF3 instance, because SharedContextOutcomeMaps reads Sign × Sign; the exchange itself is for arbitrary m × n.
• No P_st. The tables are arbitrary no-signalling tables; the singlet is not instantiated.

References: SkewFibrePartition.lean (skewCell, JointRates, eq_of_vadd_preimage_circleCell_eq), ArcAffine.lean (rectMap, map_restrict_rectMap, existsUnique_mem_circleCell), Mathlib/MeasureTheory/GluedMeasurePreserving.lean (glue, measurePreserving_glue), LF3/SettingLocalityLocal.lean (LocalSettingLocalityA/B, operationalNoSignalling_of_localSettingLocality); specs/BACKLOG.md #137, #131 obligation (4).

The normal form: bands by B's outcome, split by A's share of the column

noncomputable def CSD.RecordLayer.JointRates.colFrac {m n : ℕ} (q : JointRates m n) (t : Fin n) (s : Fin m) : ℝ

A's share of B's column t: rate s t / colSum t.

Equations

• q.colFrac t s = q.rate s t / q.colSum t

theorem CSD.RecordLayer.JointRates.colFrac_nonneg {m n : ℕ} (q : JointRates m n) (t : Fin n) (s : Fin m) : 0 ≤ q.colFrac t s

theorem CSD.RecordLayer.JointRates.sum_colFrac_of_pos {m n : ℕ} (q : JointRates m n) {t : Fin n} (h : 0 < q.colSum t) : ∑ s : Fin m, q.colFrac t s = 1

theorem CSD.RecordLayer.JointRates.colSum_mul_colFrac {m n : ℕ} (q : JointRates m n) (t : Fin n) (s : Fin m) : q.colSum t * q.colFrac t s = q.rate s t

theorem CSD.RecordLayer.JointRates.rate_pos_iff {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : 0 < q.rate s t ↔ 0 < q.rowSum s ∧ 0 < q.condRate s t

theorem CSD.RecordLayer.JointRates.colSum_pos_of_rate_pos {m n : ℕ} (q : JointRates m n) {s : Fin m} {t : Fin n} (h : 0 < q.rate s t) : 0 < q.colSum t

theorem CSD.RecordLayer.JointRates.colFrac_pos_of_rate_pos {m n : ℕ} (q : JointRates m n) {s : Fin m} {t : Fin n} (h : 0 < q.rate s t) : 0 < q.colFrac t s

def CSD.RecordLayer.normalCell {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : Set LF4.KTorus

The normal cell of the outcome pair (s, t): A's share of B's column, in θ₁, times the arc of B's marginal, in θ₂. The normal cells with the same t tile the band [0,1) × C_t.

Equations

• CSD.RecordLayer.normalCell q s t = CSD.RecordLayer.circleCell (q.colFrac t) s ×ˢ CSD.RecordLayer.circleCell q.colSum t

theorem CSD.RecordLayer.measurableSet_normalCell {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : MeasurableSet (normalCell q s t)

Both families tile the fibre exactly

theorem CSD.RecordLayer.existsUnique_mem_skewCell {m n : ℕ} (q : JointRates m n) (θ : LF4.KTorus) : ∃! st : Fin m × Fin n, θ ∈ skewCell q st.1 st.2

★ The skew cells tile the fibre exactly: every point lies in exactly one.

theorem CSD.RecordLayer.normalCell_pairwiseDisjoint {m n : ℕ} (q : JointRates m n) : Pairwise (Function.onFun Disjoint fun (st : Fin m × Fin n) => normalCell q st.1 st.2)

Distinct normal cells are disjoint: different t separate in θ₂, the same t with different s in θ₁.

theorem CSD.RecordLayer.existsUnique_mem_normalCell {m n : ℕ} (q : JointRates m n) (θ : LF4.KTorus) : ∃! st : Fin m × Fin n, θ ∈ normalCell q st.1 st.2

★ The normal cells tile the fibre exactly.

noncomputable def CSD.RecordLayer.skewIdx {m n : ℕ} (q : JointRates m n) (θ : LF4.KTorus) : Fin m × Fin n

The cell of a point, in the skew tiling.

Equations

• CSD.RecordLayer.skewIdx q θ = MeasureTheory.glueIdx ⋯ θ

theorem CSD.RecordLayer.mem_skewCell_skewIdx {m n : ℕ} (q : JointRates m n) (θ : LF4.KTorus) : θ ∈ skewCell q (skewIdx q θ).1 (skewIdx q θ).2

theorem CSD.RecordLayer.skewIdx_eq_of_mem {m n : ℕ} (q : JointRates m n) {θ : LF4.KTorus} {s : Fin m} {t : Fin n} (h : θ ∈ skewCell q s t) : skewIdx q θ = (s, t)

noncomputable def CSD.RecordLayer.normalIdx {m n : ℕ} (q : JointRates m n) (θ : LF4.KTorus) : Fin m × Fin n

The cell of a point, in the normal tiling.

Equations

• CSD.RecordLayer.normalIdx q θ = MeasureTheory.glueIdx ⋯ θ

theorem CSD.RecordLayer.mem_normalCell_normalIdx {m n : ℕ} (q : JointRates m n) (θ : LF4.KTorus) : θ ∈ normalCell q (normalIdx q θ).1 (normalIdx q θ).2

theorem CSD.RecordLayer.normalIdx_snd_eq_of_mem {m n : ℕ} (q : JointRates m n) {θ : LF4.KTorus} {t : Fin n} (h : θ.2 ∈ circleCell q.colSum t) : (normalIdx q θ).2 = t

A point of the band C_t has normal index t in the second slot.

theorem CSD.RecordLayer.rate_pos_of_mem_skewCell {m n : ℕ} (q : JointRates m n) {θ : LF4.KTorus} {s : Fin m} {t : Fin n} (h : θ ∈ skewCell q s t) : 0 < q.rate s t

Membership in a cell forces a positive rate.

theorem CSD.RecordLayer.rate_pos_of_mem_normalCell {m n : ℕ} (q : JointRates m n) {θ : LF4.KTorus} {s : Fin m} {t : Fin n} (h : θ ∈ normalCell q s t) : 0 < q.rate s t

The affine pieces

noncomputable def CSD.RecordLayer.toNormal {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : LF4.KTorus → LF4.KTorus

The piece of the normalisation: the Jacobian-one affine map of the skew cell (s, t) onto its normal cell.

Equations

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

noncomputable def CSD.RecordLayer.toSkew {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : LF4.KTorus → LF4.KTorus

The piece of the denormalisation: the inverse affine map, normal cell onto skew cell.

Equations

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

theorem CSD.RecordLayer.measurable_toNormal {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : Measurable (toNormal q s t)

theorem CSD.RecordLayer.measurable_toSkew {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : Measurable (toSkew q s t)

theorem CSD.RecordLayer.loSum_nonneg' {k : ℕ} {r : Fin k → ℝ} (hr : ∀ (i : Fin k), 0 ≤ r i) (i : Fin k) : 0 ≤ loSum r i

The lower endpoints of the cells are non-negative.

theorem CSD.RecordLayer.toNormal_mem {m n : ℕ} (q : JointRates m n) {s : Fin m} {t : Fin n} {θ : LF4.KTorus} (h : θ ∈ skewCell q s t) : toNormal q s t θ ∈ normalCell q s t

Pointwise: a point of the skew cell lands in the normal cell.

theorem CSD.RecordLayer.toSkew_mem {m n : ℕ} (q : JointRates m n) {s : Fin m} {t : Fin n} {θ : LF4.KTorus} (h : θ ∈ normalCell q s t) : toSkew q s t θ ∈ skewCell q s t

Pointwise: a point of the normal cell lands in the skew cell.

theorem CSD.RecordLayer.skewCell_eq_empty_of_rate_eq_zero {m n : ℕ} (q : JointRates m n) {s : Fin m} {t : Fin n} (h : q.rate s t = 0) : skewCell q s t = ∅

A skew cell with zero rate is empty.

theorem CSD.RecordLayer.normalCell_eq_empty_of_rate_eq_zero {m n : ℕ} (q : JointRates m n) {s : Fin m} {t : Fin n} (h : q.rate s t = 0) : normalCell q s t = ∅

A normal cell with zero rate is empty.

theorem CSD.RecordLayer.map_restrict_toNormal {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : MeasureTheory.Measure.map (toNormal q s t) (MeasureTheory.volume.restrict (skewCell q s t)) = MeasureTheory.volume.restrict (normalCell q s t)

★ The measure transport of a normalisation piece: exact, with no scalar.

theorem CSD.RecordLayer.map_restrict_toSkew {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : MeasureTheory.Measure.map (toSkew q s t) (MeasureTheory.volume.restrict (normalCell q s t)) = MeasureTheory.volume.restrict (skewCell q s t)

★ The measure transport of a denormalisation piece: exact, with no scalar.

The glued exchanges

noncomputable def CSD.RecordLayer.normalize {m n : ℕ} (q : JointRates m n) : LF4.KTorus → LF4.KTorus

The normalisation: on each skew cell, its affine piece.

Equations

• CSD.RecordLayer.normalize q = MeasureTheory.glue ⋯ fun (st : Fin m × Fin n) => CSD.RecordLayer.toNormal q st.1 st.2

noncomputable def CSD.RecordLayer.denormalize {m n : ℕ} (q : JointRates m n) : LF4.KTorus → LF4.KTorus

The denormalisation: on each normal cell, its affine piece.

Equations

• CSD.RecordLayer.denormalize q = MeasureTheory.glue ⋯ fun (st : Fin m × Fin n) => CSD.RecordLayer.toSkew q st.1 st.2

theorem CSD.RecordLayer.normalize_mem {m n : ℕ} (q : JointRates m n) {θ : LF4.KTorus} {s : Fin m} {t : Fin n} (h : θ ∈ skewCell q s t) : normalize q θ ∈ normalCell q s t

theorem CSD.RecordLayer.denormalize_mem {m n : ℕ} (q : JointRates m n) {θ : LF4.KTorus} {s : Fin m} {t : Fin n} (h : θ ∈ normalCell q s t) : denormalize q θ ∈ skewCell q s t

theorem CSD.RecordLayer.measurePreserving_normalize {m n : ℕ} (q : JointRates m n) : MeasureTheory.MeasurePreserving (normalize q) MeasureTheory.volume MeasureTheory.volume

★★ The normalisation preserves Haar measure — the gluing theorem over the exact tilings.

theorem CSD.RecordLayer.measurePreserving_denormalize {m n : ℕ} (q : JointRates m n) : MeasureTheory.MeasurePreserving (denormalize q) MeasureTheory.volume MeasureTheory.volume

★★ The denormalisation preserves Haar measure.

The reroute

noncomputable def CSD.RecordLayer.reroute {m n : ℕ} (q q' : JointRates m n) : LF4.KTorus → LF4.KTorus

The reroute from the table q to the table q': normalise along q, denormalise along q'.

Equations

• CSD.RecordLayer.reroute q q' = CSD.RecordLayer.denormalize q' ∘ CSD.RecordLayer.normalize q

theorem CSD.RecordLayer.measurePreserving_reroute {m n : ℕ} (q q' : JointRates m n) : MeasureTheory.MeasurePreserving (reroute q q') MeasureTheory.volume MeasureTheory.volume

★★ The reroute preserves Haar measure.

theorem CSD.RecordLayer.wingB_reroute {m n : ℕ} {q q' : JointRates m n} (hcol : q.colSum = q'.colSum) (θ : LF4.KTorus) : (skewIdx q' (reroute q q' θ)).2 = (skewIdx q θ).2

★★ B's reading is carried along the reroute when B's marginal is the same in both tables: the normal form of a point of B's t-region lies in the band C_t, and the band is the same for q', so the denormalisation lands in q''s t-region.

theorem CSD.RecordLayer.wingA_eq_of_rowSum_eq {m n : ℕ} {q q' : JointRates m n} (hrow : q.rowSum = q'.rowSum) (θ : LF4.KTorus) : (skewIdx q' θ).1 = (skewIdx q θ).1

A's reading does not depend on the table beyond A's marginal: with the same rowSum, the same θ₁-cell.

The LF3 instance: the I3 record basins satisfy the local-setting-aware primitive

def CSD.RecordLayer.signOfFin : Fin 2 → LF3.Sign

The outcome index as a sign: 0 ↦ plus, 1 ↦ minus.

Equations

• CSD.RecordLayer.signOfFin = ![CSD.LF3.Sign.plus, CSD.LF3.Sign.minus]

noncomputable def CSD.RecordLayer.skewOutcomeMaps (Q : LF3.MeasurementContext → JointRates 2 2) : LF3.SharedContextOutcomeMaps LF4.KTorus

The I3 outcome maps of a family of 2 × 2 joint tables, one per context: A reads the θ₁-cell of the context's table, B the conditional θ₂-cell.

Equations

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

theorem CSD.RecordLayer.measurable_skewIdx {m n : ℕ} (q : JointRates m n) : Measurable (skewIdx q)

The cell index is measurable: its level sets are the cells.

theorem CSD.RecordLayer.measurable_skewOutcomeMaps (Q : LF3.MeasurementContext → JointRates 2 2) : LF3.MeasurableSharedContextOutcomeMaps (skewOutcomeMaps Q)

def CSD.RecordLayer.skewLocalSettingLocalityA (Q : LF3.MeasurementContext → JointRates 2 2) (hrow : ∀ (a b b' : LF3.DetectorSetting), (Q { a := a, b := b }).rowSum = (Q { a := a, b := b' }).rowSum) : LF3.LocalSettingLocalityA MeasureTheory.volume (skewOutcomeMaps Q)

★★★ The A-wing primitive at the I3 basins, with the identity as reroute: A's reading does not depend on B's setting when A's marginal does not.

Equations

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

noncomputable def CSD.RecordLayer.skewLocalSettingLocalityB (Q : LF3.MeasurementContext → JointRates 2 2) (hcol : ∀ (a a' b : LF3.DetectorSetting), (Q { a := a, b := b }).colSum = (Q { a := a', b := b }).colSum) : LF3.LocalSettingLocalityB MeasureTheory.volume (skewOutcomeMaps Q)

★★★ The B-wing primitive at the I3 basins, with the skew rectangle exchange as reroute: measure-preserving, and B's reading is carried along when B's marginal does not depend on A's setting.

Equations

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

theorem CSD.RecordLayer.operationalNoSignalling_skew (Q : LF3.MeasurementContext → JointRates 2 2) (hrow : ∀ (a b b' : LF3.DetectorSetting), (Q { a := a, b := b }).rowSum = (Q { a := a, b := b' }).rowSum) (hcol : ∀ (a a' b : LF3.DetectorSetting), (Q { a := a, b := b }).colSum = (Q { a := a', b := b }).colSum) : LF3.OperationalNoSignalling MeasureTheory.volume (skewOutcomeMaps Q)

★★★ Operational no-signalling for the I3 record basins, derived from the primitive. For any family of no-signalling 2 × 2 tables, the fibre with its skew partition satisfies both local-setting-aware primitives, hence remote marginal invariance on both wings.