The skew reroute over the base: setting locality for Σ = KSigma N and the epistemic measure

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #155 (out of #137): the base-coupled version.

#137 instantiated the local-setting-aware primitive on the fibre T² with the tables as data. #135's JointContextField attaches a table to every base point and reads the skew basin skewBasin c s t = {x | x.2 ∈ skewCell (c.rates x.1) s t}. This file lifts the reroute: at x, exchange along the tables at x's own base point,

rerouteBasin c c' x = (x.1, reroute (c.rates x.1) (c'.rates x.1) x.2).

• Measurability is the work, and it is where the parameters of the affine pieces enter as measurable functions of the base point: measurable_rectMap_param (an affine rectangle map whose six parameters are measurable in the base point is jointly measurable), the regularity of the column data (measurable_colSum, measurable_colFrac, measurable_loSum_colFrac, measurable_loSum_colSum), the measurable normalBasin, and the glued maps over the base normalizeB, denormalizeB with ★ measurable_normalizeB, ★ measurable_denormalizeB — the preimage of a set splits along the finitely many skew basins, exactly as in the fibre proof.
• ★★ measurePreserving_rerouteBasin: for every preparation p, the reroute preserves epistemicMeasure p = δ_p ⊗ vol. Almost everywhere for that measure x.1 = p, so the reroute agrees a.e. with Prod.map id (reroute (c.rates p) (c'.rates p)), which preserves δ_p ⊗ vol by the fibre theorem.
• ★★ wingB_rerouteBasin, wingA_eq_of_rowSum_eq': the readings transport pointwise, from the fibre statements at the base point x.1.
• The LF3 instance on Σ: skewBasinOutcomeMaps Q for a family of joint context fields Q : MeasurementContext → JointContextField N 2 2, ★★★ skewBasinLocalSettingLocalityA/B for every p, ★★★ operationalNoSignalling_skewBasin — operational no-signalling for the I3 record basins on Σ itself, for the epistemic measure of every preparation, and ★★★ operationalNoSignalling_skewBasin_singlet for the singlet as a constant field.

Honest scope

• The no-signalling of the tables is a hypothesis at every base point (rowSum independent of b, colSum of a, pointwise in p), which is what any Born-derived joint context field satisfies and what the readings' marginals require.
• The measure is epistemicMeasure p, one preparation at a time, as everywhere in the record layer; the primitive is stated per measure, so this is the statement at the right level.
• 2 × 2 outcomes in the LF3 instance; the exchange is for arbitrary m × n.

References: SkewReroute.lean (reroute, measurePreserving_reroute, wingB_reroute, skewOutcomeMaps), SkewBasin.lean (JointContextField, skewBasin, measurableSet_skewBasin, constJointContext), SingletSkewTables.lean (singletTables), ArcAffine.lean (rectMap), LF3/SettingLocalityLocal.lean; specs/BACKLOG.md #155, #137, #135.

Regularity of the column data over the base

theorem CSD.RecordLayer.JointContextField.measurable_colSum {N m n : ℕ} (c : JointContextField N m n) (t : Fin n) : Measurable fun (p : LF4.CPN N) => (c.rates p).colSum t

theorem CSD.RecordLayer.JointContextField.measurable_colFrac {N m n : ℕ} (c : JointContextField N m n) (t : Fin n) (s : Fin m) : Measurable fun (p : LF4.CPN N) => (c.rates p).colFrac t s

theorem CSD.RecordLayer.JointContextField.measurable_loSum_colFrac {N m n : ℕ} (c : JointContextField N m n) (t : Fin n) (s : Fin m) : Measurable fun (p : LF4.CPN N) => loSum ((c.rates p).colFrac t) s

theorem CSD.RecordLayer.JointContextField.measurable_loSum_colSum {N m n : ℕ} (c : JointContextField N m n) (t : Fin n) : Measurable fun (p : LF4.CPN N) => loSum (c.rates p).colSum t

The normal basin

def CSD.RecordLayer.normalBasin {N m n : ℕ} (c : JointContextField N m n) (s : Fin m) (t : Fin n) : Set (LF4.KSigma N)

The normal basin of the outcome pair: the fibre point lies in the normal cell of the table at its own base point.

Equations

• CSD.RecordLayer.normalBasin c s t = {x : CSD.LF4.KSigma N | x.2 ∈ CSD.RecordLayer.normalCell (c.rates x.1) s t}

theorem CSD.RecordLayer.measurableSet_normalBasin {N m n : ℕ} (c : JointContextField N m n) (s : Fin m) (t : Fin n) : MeasurableSet (normalBasin c s t)

Affine rectangle maps with parameters measurable in the base point

theorem CSD.RecordLayer.measurable_rectMap_param {N : ℕ} {x₀ α lam₁ y₀ β lam₂ : LF4.CPN N → ℝ} (hx₀ : Measurable x₀) (hα : Measurable α) (hlam₁ : Measurable lam₁) (hy₀ : Measurable y₀) (hβ : Measurable β) (hlam₂ : Measurable lam₂) : Measurable fun (x : LF4.KSigma N) => rectMap (x₀ x.1) (α x.1) (lam₁ x.1) (y₀ x.1) (β x.1) (lam₂ x.1) x.2

An affine rectangle map whose six parameters are measurable functions of the base point is jointly measurable on Σ.

theorem CSD.RecordLayer.measurable_toNormal_param {N m n : ℕ} (c : JointContextField N m n) (s : Fin m) (t : Fin n) : Measurable fun (x : LF4.KSigma N) => toNormal (c.rates x.1) s t x.2

theorem CSD.RecordLayer.measurable_toSkew_param {N m n : ℕ} (c : JointContextField N m n) (s : Fin m) (t : Fin n) : Measurable fun (x : LF4.KSigma N) => toSkew (c.rates x.1) s t x.2

The glued exchanges over the base

noncomputable def CSD.RecordLayer.normalizeB {N m n : ℕ} (c : JointContextField N m n) (x : LF4.KSigma N) : LF4.KTorus

The normalisation along the table at the point's own base point.

Equations

• CSD.RecordLayer.normalizeB c x = CSD.RecordLayer.normalize (c.rates x.1) x.2

noncomputable def CSD.RecordLayer.denormalizeB {N m n : ℕ} (c : JointContextField N m n) (x : LF4.KSigma N) : LF4.KTorus

The denormalisation along the table at the point's own base point.

Equations

• CSD.RecordLayer.denormalizeB c x = CSD.RecordLayer.denormalize (c.rates x.1) x.2

theorem CSD.RecordLayer.normalizeB_eq_of_mem {N m n : ℕ} (c : JointContextField N m n) {x : LF4.KSigma N} {s : Fin m} {t : Fin n} (h : x ∈ skewBasin c s t) : normalizeB c x = toNormal (c.rates x.1) s t x.2

theorem CSD.RecordLayer.denormalizeB_eq_of_mem {N m n : ℕ} (c : JointContextField N m n) {x : LF4.KSigma N} {s : Fin m} {t : Fin n} (h : x ∈ normalBasin c s t) : denormalizeB c x = toSkew (c.rates x.1) s t x.2

theorem CSD.RecordLayer.measurable_normalizeB {N m n : ℕ} (c : JointContextField N m n) : Measurable (normalizeB c)

★ The normalisation over the base is measurable: its preimages split along the skew basins.

theorem CSD.RecordLayer.measurable_denormalizeB {N m n : ℕ} (c : JointContextField N m n) : Measurable (denormalizeB c)

★ The denormalisation over the base is measurable.

The reroute over the base

noncomputable def CSD.RecordLayer.rerouteBasin {N m n : ℕ} (c c' : JointContextField N m n) (x : LF4.KSigma N) : LF4.KSigma N

The reroute over the base: at x, exchange along the tables at x's own base point.

Equations

• CSD.RecordLayer.rerouteBasin c c' x = (x.1, CSD.RecordLayer.denormalizeB c' (x.1, CSD.RecordLayer.normalizeB c x))

theorem CSD.RecordLayer.rerouteBasin_eq {N m n : ℕ} (c c' : JointContextField N m n) (x : LF4.KSigma N) : rerouteBasin c c' x = (x.1, reroute (c.rates x.1) (c'.rates x.1) x.2)

theorem CSD.RecordLayer.measurable_rerouteBasin {N m n : ℕ} (c c' : JointContextField N m n) : Measurable (rerouteBasin c c')

theorem CSD.RecordLayer.ae_fst_eq {N : ℕ} (p : LF4.CPN N) : ∀ᵐ (x : LF4.KSigma N) ∂epistemicMeasure p, x.1 = p

Under δ_p ⊗ vol, almost every point lies over p.

theorem CSD.RecordLayer.measurePreserving_rerouteBasin {N m n : ℕ} (c c' : JointContextField N m n) (p : LF4.CPN N) : MeasureTheory.MeasurePreserving (rerouteBasin c c') (epistemicMeasure p) (epistemicMeasure p)

★★ The reroute over the base preserves the epistemic measure of every preparation. Almost everywhere for δ_p ⊗ vol the base point is p, so the reroute agrees a.e. with the fibre reroute at p in the second factor, which preserves δ_p ⊗ vol.

The readings transport

noncomputable def CSD.RecordLayer.skewBasinIdx {N m n : ℕ} (c : JointContextField N m n) (x : LF4.KSigma N) : Fin m × Fin n

The cell of a point of Σ, read at its own base point.

Equations

• CSD.RecordLayer.skewBasinIdx c x = CSD.RecordLayer.skewIdx (c.rates x.1) x.2

theorem CSD.RecordLayer.skewBasinIdx_preimage_singleton {N m n : ℕ} (c : JointContextField N m n) (st : Fin m × Fin n) : skewBasinIdx c ⁻¹' {st} = skewBasin c st.1 st.2

theorem CSD.RecordLayer.measurable_skewBasinIdx {N m n : ℕ} (c : JointContextField N m n) : Measurable (skewBasinIdx c)

theorem CSD.RecordLayer.wingB_rerouteBasin {N m n : ℕ} {c c' : JointContextField N m n} (hcol : ∀ (p : LF4.CPN N), (c.rates p).colSum = (c'.rates p).colSum) (x : LF4.KSigma N) : (skewBasinIdx c' (rerouteBasin c c' x)).2 = (skewBasinIdx c x).2

★★ B's reading is carried along the reroute over the base, when B's marginal agrees at every base point.

theorem CSD.RecordLayer.wingA_eq_of_rowSum_eq' {N m n : ℕ} {c c' : JointContextField N m n} (hrow : ∀ (p : LF4.CPN N), (c.rates p).rowSum = (c'.rates p).rowSum) (x : LF4.KSigma N) : (skewBasinIdx c' x).1 = (skewBasinIdx c x).1

A's reading does not depend on the field beyond A's marginal at the base point.

The LF3 instance on Σ

noncomputable def CSD.RecordLayer.skewBasinOutcomeMaps {N : ℕ} (Q : LF3.MeasurementContext → JointContextField N 2 2) : LF3.SharedContextOutcomeMaps (LF4.KSigma N)

The I3 outcome maps on Σ of a family of joint context fields, one per context.

Equations

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

theorem CSD.RecordLayer.measurable_skewBasinOutcomeMaps {N : ℕ} (Q : LF3.MeasurementContext → JointContextField N 2 2) : LF3.MeasurableSharedContextOutcomeMaps (skewBasinOutcomeMaps Q)

def CSD.RecordLayer.skewBasinLocalSettingLocalityA {N : ℕ} (Q : LF3.MeasurementContext → JointContextField N 2 2) (hrow : ∀ (a b b' : LF3.DetectorSetting) (p : LF4.CPN N), ((Q { a := a, b := b }).rates p).rowSum = ((Q { a := a, b := b' }).rates p).rowSum) (p : LF4.CPN N) : LF3.LocalSettingLocalityA (epistemicMeasure p) (skewBasinOutcomeMaps Q)

★★★ The A-wing primitive on Σ, identity reroute, for every preparation.

Equations

• CSD.RecordLayer.skewBasinLocalSettingLocalityA Q hrow p = { reroute := fun (x x_1 x_2 : CSD.LF3.DetectorSetting) (x_3 : CSD.LF4.KSigma N) => x_3, measurePreserving := ⋯, wingA_invariant := ⋯ }

noncomputable def CSD.RecordLayer.skewBasinLocalSettingLocalityB {N : ℕ} (Q : LF3.MeasurementContext → JointContextField N 2 2) (hcol : ∀ (a a' b : LF3.DetectorSetting) (p : LF4.CPN N), ((Q { a := a, b := b }).rates p).colSum = ((Q { a := a', b := b }).rates p).colSum) (p : LF4.CPN N) : LF3.LocalSettingLocalityB (epistemicMeasure p) (skewBasinOutcomeMaps Q)

★★★ The B-wing primitive on Σ, the rectangle exchange over the base, for every preparation.

Equations

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

theorem CSD.RecordLayer.operationalNoSignalling_skewBasin {N : ℕ} (Q : LF3.MeasurementContext → JointContextField N 2 2) (hrow : ∀ (a b b' : LF3.DetectorSetting) (p : LF4.CPN N), ((Q { a := a, b := b }).rates p).rowSum = ((Q { a := a, b := b' }).rates p).rowSum) (hcol : ∀ (a a' b : LF3.DetectorSetting) (p : LF4.CPN N), ((Q { a := a, b := b }).rates p).colSum = ((Q { a := a', b := b }).rates p).colSum) (p : LF4.CPN N) : LF3.OperationalNoSignalling (epistemicMeasure p) (skewBasinOutcomeMaps Q)

★★★ Operational no-signalling for the I3 record basins on Σ, for the epistemic measure of every preparation, derived from the primitive.

noncomputable def CSD.RecordLayer.singletField (N : ℕ) (C : LF3.MeasurementContext) : JointContextField N 2 2

The singlet's tables as a constant joint context field over the base.

Equations

• CSD.RecordLayer.singletField N C = CSD.RecordLayer.constJointContext (CSD.RecordLayer.singletTables C)

theorem CSD.RecordLayer.operationalNoSignalling_skewBasin_singlet (N : ℕ) (p : LF4.CPN N) : LF3.OperationalNoSignalling (epistemicMeasure p) (skewBasinOutcomeMaps (singletField N))

★★★ The singlet on the I3 record basins of Σ is operationally no-signalling, for every preparation, by the primitive.