A non-product record partition of T²: option I3

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #134, taken at the author's decision by the I3 route; bears on #131 obligation (3) and #132.

The question this answers, and the theorem that forces the answer

torusCell's mem_torusCell_iff records that the Born partition reads θ₁ and ignores θ₂ — "the symplectic partner carries no record content". Option I1 (#131 blocker (I)) keeps that and obtains the two wings by coarsening one selector. The objection it concedes is that x.2.2 stays inert. I3 is the other route: give the second coordinate record content.

And the choice is constrained. ★★★ volume_prodPartition_eq_mul says that if A's region is a θ₁-set and B's region a θ₂-set then the joint law is exactly the product of the marginals, and ★★★ not_exists_prodPartition_of_ne_mul turns that around: a joint law that is not the product of its own marginals has no such partition of the fibre at all.

⚠️ Read the hypothesis exactly. It is that the two wings read different coordinates — one each. So the theorem does not apply to option I1, where both wings read θ₁ and correlation is carried fine (TwoWingCoarsening.measure_coarseEvent). What it rules out is the one-coordinate-per-wing shape, and it leaves exactly two live options: the wings share a coordinate (I1), or at least one wing's region reads both (I3, below). It is the fibre-level analogue of LF6.no_product_partition_realises_singlet, proved here by Fubini rather than assumed, and it turns a claim TwoWingCoarsening's header had been making in prose — that with independent selectors the joint law factorises, so they could not carry correlation at all — into a theorem.

What is proved

• JointRates m n — a joint rate table of one joint context, with every A-marginal positive so the conditional law is defined;
• skewCell q s t — the I3 cell: A's arc in θ₁, and in θ₂ the arc of the conditional rate q s t / rowSum q s. The cells are rectangles, but the partition is not a product: the θ₂-arc moves with s;
• ★★★ volume_skewCell — exact Born weights, volume (skewCell q s t) = q s t, for an arbitrary joint law. So I3 realises any correlation, the singlet's included, with no error term;
• ★★★ volume_wingAFibre and ★★★ volume_wingBFibre — both marginals come out right: rowSum q s and colSum q t. B's is the non-trivial one — the construction never mentions colSum, so no-signalling for B is a theorem about the geometry, not something arranged;
• ★★★ not_exists_sndSet_of_condRate_ne — x.2.1 is load-bearing for B's record: when the conditional law genuinely depends on A's cell, no θ₂-set describes B's region. Together with the no-go above this is an equivalence in spirit: correlation and θ₂-nonlocality of B's region are the same fact;
• skewCell_pairwiseDisjoint, skewCell_ae_total, ★ wingAFibre_inter_wingBFibre — it is a partition, it covers T² up to a null set, and the two wing regions meet in exactly one cell;
• ★★★ eq_of_vadd_preimage_circleCell_eq — what a reroute cannot be: a rotation of the record circle preserves a cell's width, so it can never implement a change of conditional law. A LF3.RemoteSettingLocalityB relabelling at the record-layer basins therefore cannot be a fibrewise rotation, which rules out the cheapest candidate the #131 audit suggested.

The finding: I2 and I3 are the same construction

#132 listed I2 (chained selectors — a second selector whose rates depend on the first's outcome) and I3 (a non-product partition of T²) as two alternatives. They are not two. A partition of T² that carries correlation must, by the no-go above, have a wing reading both coordinates; writing the joint law as marginal-times-conditional is then the chain rule, and condRate is that conditional. So the construction below is simultaneously I2 and I3, and the author's choice is binary — I1's single coarsened selector, or this — not ternary. The order (A first, B conditional) is the chain rule's arbitrary choice and carries no physical content; the mirror construction with the roles swapped realises the same joint law.

Honest scope

⚠️ This is the fibre only. The rates are an argument; nothing here is attached to a base point, so there is no ContextField, no globalBasin and no epistemicMeasure. Coupling it to the base — a joint-context field and its skew basin, which is what would let this replace globalBasin — is the continuation, priced as #135.

⚠️ No P_st, no Bell. The joint law is arbitrary. The singlet is not mentioned, and nothing here computes a CHSH value or claims a Bell violation. What is shown is that the fibre can carry any joint law exactly, and that it must be non-product to do so.

✅ No positivity hypothesis (rowPos dropped 2026-10-11, BACKLOG #136). An A-outcome of probability zero has no conditional law, and an earlier version of this file demanded strictly positive A-marginals for that reason. It is not needed: Lean's x / 0 = 0 gives a null row condRate = 0, and non-negativity forces the whole row to vanish with its sum (rate_eq_zero_of_rowSum_eq_zero), so ★ rowSum_mul_condRate and ★ loSum_condRate_le_one both hold by a case split. The null row simply contributes an empty θ₂ cell of measure zero. Positivity survives only where it is genuinely needed, as an explicit hypothesis of not_exists_sndSet_of_condRate_ne — a null A-cell has no second coordinate to be non-local in.

⚠️ I3 does not make the two wings symmetric. A's region is a θ₁-set; it is B's that reads both coordinates. The no-go only forces one wing to be non-local, and the chain rule picks which. Calling the result "two independent selectors" would be wrong: there are two coordinates, both load-bearing, and one conditional dependence between them.

⚠️ Nothing here is a claim about Σ's dynamics. Whether a flow writes these cells is MacrostateStability's and LF6's business and is untouched.

References: TorusFibre.lean (torusCell, mem_torusCell_iff — the statement this file is the alternative to), CircleFibre.lean (circleCell, volume_circleCell, loSum), BornFibrePartition.lean (loSum), TwoWingCoarsening.lean (option I1, the alternative), LF6/ForcedContextuality.lean (no_product_partition_realises_singlet, the base-level analogue of this file's no-go); specs/BACKLOG.md #134, #132, #131 obligation (3), #135; specs/sigma-fibre-contextuality.md (probabilities Born, regions contextual).

A product fibre partition cannot correlate

theorem CSD.RecordLayer.volume_prodPartition_eq_mul (S T : Set CircleFibre) : MeasureTheory.volume (S ×ˢ Set.univ ∩ Set.univ ×ˢ T) = MeasureTheory.volume S * MeasureTheory.volume T

★★★ A product fibre partition factorises the joint law, exactly. If one wing's region is a θ₁-set and the other's a θ₂-set, the measure of their intersection is the product of their measures — by Fubini, with no hypothesis on the sets beyond measurability of the ambient product measure. This is why x.2.2 has to acquire record content before the fibre can correlate.

theorem CSD.RecordLayer.not_exists_prodPartition_of_ne_mul {m n : ℕ} (q : Fin m → Fin n → ℝ) (hq : ∀ (s : Fin m) (t : Fin n), 0 ≤ q s t) {s₀ : Fin m} {t₀ : Fin n} (hne : q s₀ t₀ ≠ (∑ t : Fin n, q s₀ t) * ∑ s : Fin m, q s t₀) : ¬∃ (S : Fin m → Set CircleFibre) (T : Fin n → Set CircleFibre), (∀ (s : Fin m), MeasureTheory.volume (S s) = ENNReal.ofReal (∑ t : Fin n, q s t)) ∧ (∀ (t : Fin n), MeasureTheory.volume (T t) = ENNReal.ofReal (∑ s : Fin m, q s t)) ∧ ∀ (s : Fin m) (t : Fin n), MeasureTheory.volume (S s ×ˢ Set.univ ∩ Set.univ ×ˢ T t) = ENNReal.ofReal (q s t)

★★★ No product partition of the fibre carries a correlated joint law. A joint law that differs from the product of its own marginals at even one cell cannot be realised by a θ₁-reading wing and a θ₂-reading wing. The fibre-level analogue of LF6.no_product_partition_realises_singlet, and the reason option I3 is needed at all.

A joint rate table

structure CSD.RecordLayer.JointRates (m n : ℕ) : Type

The joint outcome probabilities of one joint context. No positivity of the A-marginals is required: a null row gets condRate = 0 through x / 0 = 0, and every identity below survives it because non-negativity forces the whole row to vanish with its sum.

• rate : Fin m → Fin n → ℝ

  The joint probability of the outcome pair.

• nonneg (s : Fin m) (t : Fin n) : 0 ≤ self.rate s t

  Joint probabilities are non-negative.

• sum_one : ∑ s : Fin m, ∑ t : Fin n, self.rate s t = 1

  The table is normalised.

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

A's marginal.

Equations

• q.rowSum s = ∑ t : Fin n, q.rate s t

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

B's marginal.

Equations

• q.colSum t = ∑ s : Fin m, q.rate s t

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

The conditional law of B given A's cell — the dependence that carries the correlation.

Equations

• q.condRate s t = q.rate s t / q.rowSum s

theorem CSD.RecordLayer.JointRates.rowSum_nonneg {m n : ℕ} (q : JointRates m n) (s : Fin m) : 0 ≤ q.rowSum s

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

A null row is null entrywise. Non-negativity turns a vanishing A-marginal into a vanishing joint rate, which is what lets the positivity hypothesis go.

theorem CSD.RecordLayer.JointRates.colSum_nonneg {m n : ℕ} (q : JointRates m n) (t : Fin n) : 0 ≤ q.colSum t

theorem CSD.RecordLayer.JointRates.sum_rowSum {m n : ℕ} (q : JointRates m n) : ∑ s : Fin m, q.rowSum s = 1

theorem CSD.RecordLayer.JointRates.sum_colSum {m n : ℕ} (q : JointRates m n) : ∑ t : Fin n, q.colSum t = 1

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

theorem CSD.RecordLayer.JointRates.condRate_eq_zero_of_rowSum_eq_zero {m n : ℕ} (q : JointRates m n) {s : Fin m} (h : q.rowSum s = 0) (t : Fin n) : q.condRate s t = 0

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

The conditional law is a probability vector on a non-null row, and identically zero on a null one — which is why loSum_condRate_le_one holds either way.

theorem CSD.RecordLayer.JointRates.rowSum_mul_condRate {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : q.rowSum s * q.condRate s t = q.rate s t

★ rowSum · condRate = rate, with no positivity hypothesis. On a null row both sides vanish, by rate_eq_zero_of_rowSum_eq_zero; off it, the division cancels.

theorem CSD.RecordLayer.JointRates.loSum_rowSum_le_one {m n : ℕ} (q : JointRates m n) (s : Fin m) : loSum q.rowSum s + q.rowSum s ≤ 1

theorem CSD.RecordLayer.JointRates.loSum_condRate_le_one {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : loSum (q.condRate s) t + q.condRate s t ≤ 1

★ The conditional cells fit in one turn, null rows included. On a null row every conditional rate is 0, so the bound is 0 ≤ 1 and nothing needs the row to be positive.

The I3 cell

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

The I3 cell: A's arc in the first torus coordinate, and in the second the arc of the conditional rate. Each cell is a rectangle, but the partition is not a product — the θ₂-arc moves with s, and that is what carries the correlation.

Equations

• CSD.RecordLayer.skewCell q s t = CSD.RecordLayer.circleCell q.rowSum s ×ˢ CSD.RecordLayer.circleCell (q.condRate s) t

@[simp]

theorem CSD.RecordLayer.mem_skewCell_iff {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) (x : LF4.KTorus) : x ∈ skewCell q s t ↔ x.1 ∈ circleCell q.rowSum s ∧ x.2 ∈ circleCell (q.condRate s) t

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

theorem CSD.RecordLayer.volume_skewCell {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : MeasureTheory.volume (skewCell q s t) = ENNReal.ofReal (q.rate s t)

★★★ Exact Born weights, for an arbitrary joint law. The cell's area is the joint probability: rowSum · condRate = rate. So I3 realises any correlation on the fibre with no error term — the singlet's included.

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

Distinct outcome pairs are mutually exclusive. Two cases: different A-outcomes already separate in θ₁; the same A-outcome with different B-outcomes separate in θ₂, because within one A-cell the conditional rate vector is the same.

The two wing regions

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

A's record region: A recorded s, whatever B recorded.

Equations

• CSD.RecordLayer.wingAFibre q s = ⋃ (t : Fin n), CSD.RecordLayer.skewCell q s t

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

B's record region: B recorded t, whatever A recorded.

Equations

• CSD.RecordLayer.wingBFibre q t = ⋃ (s : Fin m), CSD.RecordLayer.skewCell q s t

theorem CSD.RecordLayer.wingAFibre_inter_wingBFibre {m n : ℕ} (q : JointRates m n) (s : Fin m) (t : Fin n) : wingAFibre q s ∩ wingBFibre q t = skewCell q s t

★ The two wing regions meet in exactly one cell — not merely up to a null set. So the joint outcome really is the pair of wing outcomes.

theorem CSD.RecordLayer.volume_wingAFibre {m n : ℕ} (q : JointRates m n) (s : Fin m) : MeasureTheory.volume (wingAFibre q s) = ENNReal.ofReal (q.rowSum s)

★★★ A's marginal is rowSum.

theorem CSD.RecordLayer.volume_wingBFibre {m n : ℕ} (q : JointRates m n) (t : Fin n) : MeasureTheory.volume (wingBFibre q t) = ENNReal.ofReal (q.colSum t)

★★★ B's marginal is colSum — no-signalling for B, as a theorem about the geometry. The construction never mentions colSum: B's cells were built from the conditional rates, and summing them over A's cells returns B's marginal because rowSum · condRate = rate. Nothing was arranged to make this come out.

x.2.1 is load-bearing for B's record

theorem CSD.RecordLayer.not_exists_sndSet_of_condRate_ne {m n : ℕ} (q : JointRates m n) {s₁ s₂ : Fin m} {t : Fin n} (hp₁ : 0 < q.rowSum s₁) (hp₂ : 0 < q.rowSum s₂) (hne : q.condRate s₁ t ≠ q.condRate s₂ t) : ¬∃ (T : Set CircleFibre), ∀ (s : Fin m), skewCell q s t = circleCell q.rowSum s ×ˢ T

★★★ B's record region is not a θ₂-set. If some single second-coordinate set T described B's outcome t across all of A's cells, then the conditional law of B given A would be the same in every A-cell. So exactly when the conditional law genuinely depends on A's cell — exactly when there is correlation — the first torus coordinate is load-bearing for B's record, and the partition is not a product.

With volume_prodPartition_eq_mul this is the two sides of one fact: correlation and the θ₂-nonlocality of B's region are the same thing.

What a reroute cannot be

LF3.RemoteSettingLocalityB asks for a measure-preserving relabelling of Σ under which B's reading is unchanged when A's setting moves. At the record-layer basins B's reading is an arc of the second coordinate whose width is the conditional rate, and the audit of #131 suggested the relabelling would be a rotation (or piecewise rotation) of the record circle. The next theorem says it cannot be: a translation preserves Haar measure, so it preserves an arc's width, while a change of A's setting changes the conditional width.

theorem CSD.RecordLayer.eq_of_vadd_preimage_circleCell_eq {k : ℕ} (r r' : Fin k → ℝ) (hr : ∀ (i : Fin k), 0 ≤ r i) (hr' : ∀ (i : Fin k), 0 ≤ r' i) (hs : ∀ (i : Fin k), loSum r i + r i ≤ 1) (hs' : ∀ (i : Fin k), loSum r' i + r' i ≤ 1) (c : CircleFibre) (i : Fin k) (h : (fun (θ : CircleFibre) => θ + c) ⁻¹' circleCell r' i = circleCell r i) : r i = r' i

★★★ A rotation cannot change a cell's width. If translating the record circle by c carries the cell of r' onto the cell of r, then r i = r' i — because translation preserves Haar measure and a cell's measure is its rate.

So a rotation of the record coordinate can never implement a change of conditional law, and a LF3.RemoteSettingLocalityB reroute at the record-layer basins cannot be a fibrewise rotation: it has to move mass between A's cells. That is permitted — the B-wing primitive constrains only wingB — but it means the two wings' relabellings cannot be built from one fibrewise family, and it rules out the cheapest candidate construction.

Totality

theorem CSD.RecordLayer.skewCell_ae_total {m n : ℕ} (q : JointRates m n) : MeasureTheory.volume (Set.univ \ ⋃ (st : Fin m × Fin n), skewCell q st.1 st.2) = 0

The cells cover T² up to a null set, so a.e. microstate of the fibre yields a joint record.