The joint moment context: an I3 rate field that comes from the base

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #136, the open half of it.

SkewBasin.lean built the skew-cell record layer (I3) over an arbitrary JointContextField, and exhibited exactly one: constJointContext, whose table does not move with the ontic point. I1 has momentContext, whose rates are the Born weights of the base point, so the I1/I3 comparison was not like for like. This file supplies I3's analogue, and the comparison becomes a theorem rather than a remark.

• jointMomentContext b — the joint field of a degeneracy map b : Fin N → Fin m × Fin n: the joint rate of the outcome pair (s, t) is the moment map summed over the directions b sends to that pair. Every field condition comes from the moment map's, as it does for blockField;
• ★★★ jointMomentContext_rowSum — A's marginal is blockField's rate at A's coarsening. This is the parity statement: the wing-A reading of I3 at this field is the I1 reading at the same coarse-graining, not merely analogous to it. ★★ jointMomentContext_colSum is B's half;
• ★★★ skewBasin_prob_jointMomentContext — so the skew basins carry the block-coarsened Born weights, which is what makes the field a record layer rather than a table;
• ★ jointMomentContext_rowSum_single — the nondegenerate recovery: at n = 1 with b j = (j, 0) A's marginal is momentContext's rate, so I1 is the degenerate case of this field and not a separate construction.

What was reused rather than rebuilt

blockField (OutcomeField.lean) is the single-index version of this construction and already existed: the same finite sum of moment coordinates, with the same three obligations discharged the same way. It cannot be instantiated here, because OutcomeField N K indexes its outcomes by Fin K while a joint table is indexed by a product, and bridging that through Fin m × Fin n ≃ Fin (m * n) would make the definition unreadable for no gain. So the definition is written out and the relationship is proved instead — jointMomentContext_rowSum and jointMomentContext_colSum are the two statements that say this is blockField coarsened on each wing, which is the honest substitute for literal reuse.

Honest scope

⚠️ The degeneracy map is a posit, as it is for I1. b says which directions of ℂℙ^{N-1} the apparatus cannot tell apart, in both wings at once. Nothing derives it; POSITS.md Posit 10 is where that sits, and this file changes nothing about it.

⚠️ No correlation is created. The joint table is whatever the moment map and b make it: for a b whose two components are independent of each other on the support, the table factorises. A correlated table at a moving base point is this field at a b that entangles the two coordinates, and which b the two-wing experiment wants is the question SkewBasin.lean's constJointContext sidestepped by fixing the table by hand.

⚠️ This is the field, not the comparison. It puts I3's rates on the same footing as I1's; it does not re-run I1's theorems at I3, and POSITS.md's decision between the two readings is unaffected.

References: SkewBasin.lean (JointContextField, skewBasin, skewBasin_prob, constJointContext), OutcomeField.lean (blockField, the single-index original), GlobalBasin.lean (momentContext, I1's field), SkewFibrePartition.lean (JointRates, rowSum, colSum); specs/POSITS.md Posit 10; specs/BACKLOG.md #136, #135, #134.

The field

noncomputable def CSD.RecordLayer.jointMomentContext {N m n : ℕ} (b : Fin N → Fin m × Fin n) : JointContextField N m n

The joint moment context: the moment map, coarse-grained by a degeneracy map that assigns each direction to a pair of wing outcomes. This is blockField with a product index, and every field condition comes from the moment map's in the same way.

Equations

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

@[simp]

theorem CSD.RecordLayer.jointMomentContext_rate {N m n : ℕ} (b : Fin N → Fin m × Fin n) (p : LF4.CPN N) (s : Fin m) (t : Fin n) : (jointMomentContext b).rate p s t = ∑ j : Fin N with b j = (s, t), Projectivization.momentMap p j

Parity with I1: the marginals are blockField

theorem CSD.RecordLayer.jointMomentContext_rowSum {N m n : ℕ} (b : Fin N → Fin m × Fin n) (p : LF4.CPN N) (s : Fin m) : ((jointMomentContext b).rates p).rowSum s = (blockField fun (j : Fin N) => (b j).1).rate p s

★★★ A's marginal is blockField's rate at A's coarsening.

This is the statement #136 wanted: wing A's reading under I3 at this field is the I1 reading at the coarse-graining b induces on A, so the two layers are comparable at the level of rates rather than by analogy. The proof is one regrouping: the fibres of b over (s, ·) partition the fibre of (b ·).1 over s.

theorem CSD.RecordLayer.jointMomentContext_colSum {N m n : ℕ} (b : Fin N → Fin m × Fin n) (p : LF4.CPN N) (t : Fin n) : ((jointMomentContext b).rates p).colSum t = (blockField fun (j : Fin N) => (b j).2).rate p t

★★ And B's marginal is blockField's rate at B's coarsening.

The record layer at this field

theorem CSD.RecordLayer.skewBasin_prob_jointMomentContext {N m n : ℕ} (b : Fin N → Fin m × Fin n) (s : Fin m) (t : Fin n) (p : LF4.CPN N) : (epistemicMeasure p) (skewBasin (jointMomentContext b) s t) = ENNReal.ofReal (∑ j : Fin N with b j = (s, t), Projectivization.momentMap p j)

★★★ The skew basins carry the block-coarsened Born weights. skewBasin_prob is generic in the field, so this is immediate once the field exists — which is the point of building the field rather than a table: the record layer was already waiting for it.

theorem CSD.RecordLayer.jointMomentContext_rowSum_single {N : ℕ} (p : LF4.CPN N) (s : Fin N) : ((jointMomentContext fun (j : Fin N) => (j, 0)).rates p).rowSum s = (momentContext N).rate p s

★ I1 is the degenerate case, not a separate construction. At one B-outcome and the identity degeneracy on A, wing A's marginal is momentContext's rate — the same recovery blockField_id records for the single-index field.