The lower-rank factor of a coherent basis (R4 converse piece 3, #107)

The factor coordinates whose anchors have cardinality below n: the structural object the rank induction conditions on.

Why the factor, not the latents

The conditioning factor must be described by the basis coordinates, not by the latents that will eventually encode them. A latent normally carries randomness beyond the factor it represents — already 1_{U < p} generates strictly less than U — so a σ-algebra generated by latents is typically strictly larger than the factor. Everything here is therefore stated about lowerFactorMap, and the coupling to latents is deliberately absent: it belongs to the augmented-induction layer, which should consume a settled lower-factor API rather than be mixed with it.

The generation statement

Only

comap (lowerFactorMap n) inferInstance ≤ lowerRankAlgebra n

together with an eventwise mod-null converse. No raw equality is asserted or supplied by this construction; the available converse is eventwise modulo M.law. That is the same discipline as everywhere else in this layer, and for the same reason.

LowerIndex n is not closed under the Boolean operations: two small anchors can combine to a large one. That is not a defect and no closure should be engineered — the product σ-algebra on LowerFactorSpace n still contains Boolean combinations of the coordinates.

How generation is proved

Support by support, never through the iSup. The finite-factor projection lowerToFactorProjection exhibits factorMap A as a coordinate restriction of lowerFactorMap n whenever A.card < n, so exists_comap_factorMap_ae_eq already gives a representative measurable for the lower-rank factor. The containments are then joined inside eventuallyMeasurableSpace, which is a σ-algebra: the completion is the closure device, and no family of a.e. witnesses is ever chosen simultaneously.

Contents

• LowerIndex / LowerFactorSpace / lowerFactorMap, with comap_lowerFactorMap_le;
• lowerFactorProjection and lowerToFactorProjection — rank nesting and single-support restriction, whose compatibilities with the factor maps are definitional;
• exists_comap_lowerFactorMap_ae_eq — the eventwise converse to comap_lowerFactorMap_le;
• lowerIndexEquiv / comap_relabel_comap_lowerFactorMap — FinSuppPerm equivariance, with the action laws as honest equalities of equivalences and the nesting square lowerFactorProjection_lowerFactorSpaceEquiv;
• comap_lowerFactorMap_zero (raw, ⊥) and exists_comap_lowerFactorMap_one_ae_eq (the rank-one base, on the original law).

The lower-rank index and factor space

def RelSignature.CoherentBasis.LowerIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Type u

The indices of rank below n: basis coordinates whose anchor has cardinality < n.

Equations

• B.LowerIndex n = { i : B.ι // (B.anchor i).card < n }

instance RelSignature.CoherentBasis.instCountableLowerIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Countable (B.LowerIndex n)

instance RelSignature.CoherentBasis.instIsEmptyLowerIndexOfNatNat {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) : IsEmpty (B.LowerIndex 0)

At rank bound 0 there are no such indices.

@[reducible, inline]

abbrev RelSignature.CoherentBasis.LowerFactorSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Type u

The lower-rank factor space, standard Borel since the index is countable.

Equations

• B.LowerFactorSpace n = (B.LowerIndex n → Bool)

instance RelSignature.CoherentBasis.instStandardBorelSpaceLowerFactorSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : StandardBorelSpace (B.LowerFactorSpace n)

instance RelSignature.CoherentBasis.instSubsingletonLowerFactorSpaceOfNatNat {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) : Subsingleton (B.LowerFactorSpace 0)

At rank bound 0 the factor space is a single point.

noncomputable def RelSignature.CoherentBasis.lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : S.RelStructure S.Vinfinite → B.LowerFactorSpace n

The lower-rank factor map: evaluate every basis event anchored below rank n.

Equations

• B.lowerFactorMap n X i = decide (X ∈ B.event ↑i)

Measurability

theorem RelSignature.CoherentBasis.measurable_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Measurable (B.lowerFactorMap n)

The lower-rank factor map is measurable for lowerRankAlgebra n: each coordinate is the indicator of an event whose anchor has rank < n.

theorem RelSignature.CoherentBasis.comap_lowerFactorMap_le {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : MeasurableSpace.comap (B.lowerFactorMap n) inferInstance ≤ RelStructure.lowerRankAlgebra n

The pullback lands inside the conditioning factor. This is one half of the generation statement; the converse is eventwise and modulo the law.

theorem RelSignature.CoherentBasis.measurable_lowerFactorMap' {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Measurable (B.lowerFactorMap n)

The lower-rank factor map is measurable for the ambient σ-algebra too.

Rank nesting

def RelSignature.CoherentBasis.lowerIndexEmbedding {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {n m : ℕ} (h : n ≤ m) : B.LowerIndex n → B.LowerIndex m

The index embedding for n ≤ m: a smaller rank bound admits fewer coordinates.

Equations

• B.lowerIndexEmbedding h i = ⟨↑i, ⋯⟩

def RelSignature.CoherentBasis.lowerFactorProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {n m : ℕ} (h : n ≤ m) : B.LowerFactorSpace m → B.LowerFactorSpace n

The factor projection for n ≤ m: ordinary coordinate restriction.

Equations

• B.lowerFactorProjection h f = f ∘ B.lowerIndexEmbedding h

theorem RelSignature.CoherentBasis.measurable_lowerFactorProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {n m : ℕ} (h : n ≤ m) : Measurable (B.lowerFactorProjection h)

theorem RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {n m : ℕ} (h : n ≤ m) : B.lowerFactorProjection h ∘ B.lowerFactorMap m = B.lowerFactorMap n

The projection is compatible with the factor maps — definitional, since both sides read the same coordinates.

theorem RelSignature.CoherentBasis.lowerFactorProjection_comp {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) : B.lowerFactorProjection hnm ∘ B.lowerFactorProjection hmk = B.lowerFactorProjection ⋯

The projection cocycle, likewise definitional.

Restriction to a single support

def RelSignature.CoherentBasis.basisIndexToLowerIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card < n) : B.BasisIndex A → B.LowerIndex n

Every coordinate anchored inside A has rank below n, when A itself does.

Equations

• B.basisIndexToLowerIndex hA i = ⟨↑i, ⋯⟩

def RelSignature.CoherentBasis.lowerToFactorProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card < n) : B.LowerFactorSpace n → B.FactorSpace A

The finite-factor projection: restrict the lower-rank factor to the coordinates of a single support of rank < n. This is the device that lets the generation argument work support by support, rather than trying to assemble representatives through the iSup.

Equations

• B.lowerToFactorProjection hA f = f ∘ B.basisIndexToLowerIndex hA

theorem RelSignature.CoherentBasis.measurable_lowerToFactorProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card < n) : Measurable (B.lowerToFactorProjection hA)

theorem RelSignature.CoherentBasis.lowerToFactorProjection_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card < n) : B.lowerToFactorProjection hA ∘ B.lowerFactorMap n = B.factorMap A

Compatibility with the single-support factor map, definitional: reading the A-anchored coordinates of the lower-rank factor is the factor map at A.

Generation

theorem RelSignature.CoherentBasis.comap_factorMap_le_comap_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card < n) : MeasurableSpace.comap (B.factorMap A) inferInstance ≤ MeasurableSpace.comap (B.lowerFactorMap n) inferInstance

Coordinates anchored in a support of rank < n are read by the lower-rank factor: the single-support pullback sits inside the lower-rank pullback.

theorem RelSignature.CoherentBasis.fixingAlgebra_le_eventually_comap_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card < n) : RelStructure.fixingAlgebra A ≤ eventuallyMeasurableSpace (MeasurableSpace.comap (B.lowerFactorMap n) inferInstance) (MeasureTheory.ae ↑M.law)

Every event of a low-rank fixing algebra has a representative measurable for the lower-rank factor. This is proved support by support, through lowerToFactorProjection; assembling representatives directly through the iSup would require simultaneous a.e. choices and is not what happens here.

theorem RelSignature.CoherentBasis.lowerRankAlgebra_le_eventually_comap_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : RelStructure.lowerRankAlgebra n ≤ eventuallyMeasurableSpace (MeasurableSpace.comap (B.lowerFactorMap n) inferInstance) (MeasureTheory.ae ↑M.law)

The lower-rank conditioning algebra is contained in the completed lower-rank factor. Taking the iSup is legitimate here precisely because the containment is into a σ-algebra — the completion is the closure device, so no a.e. witnesses are ever joined.

theorem RelSignature.CoherentBasis.exists_comap_lowerFactorMap_ae_eq {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) {E : Set (S.RelStructure S.Vinfinite)} (hE : MeasurableSet E) : ∃ (E' : Set (S.RelStructure S.Vinfinite)), MeasurableSet E' ∧ E' =ᵐ[↑M.law] E

The eventwise converse to comap_lowerFactorMap_le: every event of the lower-rank conditioning algebra agrees, up to a null set, with an event read off the lower-rank factor.

Stated eventwise on purpose. No raw equality is asserted or supplied by this construction; the available converse is eventwise modulo M.law. Nothing here rules out an equality of the two σ-algebras — the point is that this argument does not produce one, and phrasing the converse as an equality "modulo null sets" would commit to a trim/completion identification that is not available.

Equivariance

noncomputable def RelSignature.CoherentBasis.lowerIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : B.LowerIndex n ≃ B.LowerIndex n

A relabeling as an equivalence of the lower-rank index. Unlike basisIndexEquiv, this is an equivalence of a single type: a relabeling transports anchors by an injective image map, so it preserves cardinality and hence rank.

Equations

• B.lowerIndexEquiv σ n = { toFun := fun (i : B.LowerIndex n) => ⟨B.act σ ↑i, ⋯⟩, invFun := fun (j : B.LowerIndex n) => ⟨B.act σ⁻¹ ↑j, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RelSignature.CoherentBasis.lowerIndexEquiv_apply_coe {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) (i : B.LowerIndex n) : ↑((B.lowerIndexEquiv σ n) i) = B.act σ ↑i

@[simp]

theorem RelSignature.CoherentBasis.lowerIndexEquiv_symm_apply_coe {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) (j : B.LowerIndex n) : ↑((B.lowerIndexEquiv σ n).symm j) = B.act σ⁻¹ ↑j

@[simp]

theorem RelSignature.CoherentBasis.lowerIndexEquiv_one {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : B.lowerIndexEquiv 1 n = Equiv.refl (B.LowerIndex n)

Identity, as an honest equality of equivalences. Unlike basisIndexEquiv, whose codomain BasisIndex (A.image σ) varies with σ, these are automorphisms of one fixed type, so the action laws need no dependent transport.

@[simp]

theorem RelSignature.CoherentBasis.lowerIndexEquiv_mul {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ τ : ↥S.FinSuppPerm) (n : ℕ) : B.lowerIndexEquiv (σ * τ) n = (B.lowerIndexEquiv τ n).trans (B.lowerIndexEquiv σ n)

Composition, likewise an honest equality of equivalences.

theorem RelSignature.CoherentBasis.lowerFactorMap_lowerIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) (X : S.RelStructure S.Vinfinite) (i : B.LowerIndex n) : B.lowerFactorMap n X ((B.lowerIndexEquiv σ n) i) = B.lowerFactorMap n (RelStructure.relabel (↑σ) X) i

Naturality of the lower-rank factor map, with the orientation forced, as for factorMap_basisIndexEquiv, by event_act being a preimage equality.

noncomputable def RelSignature.CoherentBasis.lowerFactorSpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : B.LowerFactorSpace n ≃ᵐ B.LowerFactorSpace n

A relabeling as a measurable automorphism of the lower-rank factor space, namely coordinate reindexing along lowerIndexEquiv.

Equations

• B.lowerFactorSpaceEquiv σ n = { toEquiv := (B.lowerIndexEquiv σ n).symm.arrowCongr (Equiv.refl Bool), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem RelSignature.CoherentBasis.lowerFactorSpaceEquiv_apply {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) (g : B.LowerFactorSpace n) (i : B.LowerIndex n) : (B.lowerFactorSpaceEquiv σ n) g i = g ((B.lowerIndexEquiv σ n) i)

@[simp]

theorem RelSignature.CoherentBasis.lowerFactorSpaceEquiv_one {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : B.lowerFactorSpaceEquiv 1 n = MeasurableEquiv.refl (B.LowerFactorSpace n)

The identity acts trivially. Reindexing is contravariant, so the composition law below reverses the order.

@[simp]

theorem RelSignature.CoherentBasis.lowerFactorSpaceEquiv_mul {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ τ : ↥S.FinSuppPerm) (n : ℕ) : B.lowerFactorSpaceEquiv (σ * τ) n = (B.lowerFactorSpaceEquiv σ n).trans (B.lowerFactorSpaceEquiv τ n)

theorem RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorSpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) {n m : ℕ} (h : n ≤ m) : B.lowerFactorProjection h ∘ ⇑(B.lowerFactorSpaceEquiv σ m) = ⇑(B.lowerFactorSpaceEquiv σ n) ∘ B.lowerFactorProjection h

The nesting/equivariance square: restricting the rank commutes with relabeling. Both sides read the coordinate act σ i of the same argument, so the identity is definitional up to proof irrelevance in the rank bound.

This is the structural coherence the rank recursion needs: without it, the relabeling action on the lower-rank factors would not descend along the nesting maps, and the actions at different ranks would be unrelated.

theorem RelSignature.CoherentBasis.lowerFactorSpaceEquiv_comp_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : ⇑(B.lowerFactorSpaceEquiv σ n) ∘ B.lowerFactorMap n = B.lowerFactorMap n ∘ RelStructure.relabel ↑σ

The relabeling of a structure is read by the factor through that automorphism.

theorem RelSignature.CoherentBasis.comap_relabel_comap_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : MeasurableSpace.comap (RelStructure.relabel ↑σ) (MeasurableSpace.comap (B.lowerFactorMap n) inferInstance) = MeasurableSpace.comap (B.lowerFactorMap n) inferInstance

The lower-rank factor pullback is relabeling invariant under the finitely supported relabelings — the factor-level counterpart of RelStructure.comap_relabel_lowerRankAlgebra, which is what makes the pullback a legitimate conditioning factor for an exchangeable law.

The degenerate ranks

theorem RelSignature.CoherentBasis.comap_lowerFactorMap_zero {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) : MeasurableSpace.comap (B.lowerFactorMap 0) inferInstance = ⊥

Rank zero is trivial on the nose — not merely modulo the law. There are no coordinates of rank below 0, so the factor space is a point and its pullback is ⊥.

theorem RelSignature.CoherentBasis.exists_comap_lowerFactorMap_one_ae_eq {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {E : Set (S.RelStructure S.Vinfinite)} (hE : MeasurableSet E) : ∃ (E' : Set (S.RelStructure S.Vinfinite)), MeasurableSet E' ∧ E' =ᵐ[↑M.law] E

Rank one: every invariant event agrees with an event of the rank-one factor, up to a null set. This is the base of the rank recursion, stated on the original law — no augmented space and no coupling.