The lower-rank conditioning algebra (R4 converse piece 3, #107)

The conditioning factor for the rankwise relative-independence theorem: the join of the fixing σ-algebras of all vertex sets of rank below n,

lowerRankAlgebra n = ⨆ A, ⨆ (_ : A.card < n), fixingAlgebra A.

Why a single global factor

The target theorem is that, for a finite family F of distinct vertex sets of rank exactly n, the exact-anchor layers at those sets are mutually — not merely pairwise — conditionally independent given everything of lower rank:

E[∏ A ∈ F, g A ∘ exactMap A | lowerRankAlgebra n] =ᵐ ∏ A ∈ F, E[g A ∘ exactMap A | lowerRankAlgebra n]

The conditioning must be this one global algebra, not a chain and not a separate conditioning per pair. Two things go wrong otherwise:

• pairwise conditional independence does not imply mutual conditional independence, so the finite-product identity cannot be assembled from two-set statements; and
• conditional independence is not preserved when the conditioning algebra is enlarged, so a statement proved against one conditioning factor cannot simply be re-read against another.

RelSignature.InfiniteRelExchangeableLaw.condIndep_fixingAlgebra therefore serves here as infrastructure and as a regression check on the two-set case, not as the proof engine. The missing finite-family statement is analogous to Austin's Proposition 3.12 (arXiv:0801.1698); its proof belongs to the downstream rankwise coupling/induction layer and is deliberately not fixed here.

This file is law-free: it defines the conditioning factor and its order theory only.

Contents

• RelStructure.lowerRankAlgebra — the conditioning factor, with _le (below the ambient algebra), _mono (monotone in the rank bound), fixingAlgebra_le_lowerRankAlgebra (each low-rank factor sits inside it), and the degenerate values at ranks 0 and 1.

@[implicit_reducible]

noncomputable def RelSignature.RelStructure.lowerRankAlgebra {S : RelSignature} (n : ℕ) : MeasurableSpace (S.RelStructure S.Vinfinite)

The lower-rank conditioning algebra: the join of the fixing σ-algebras of all vertex sets of cardinality strictly below n.

Equations

• RelSignature.RelStructure.lowerRankAlgebra n = ⨆ (A : Finset ((s : S.Srt) × S.Vinfinite s)), ⨆ (_ : A.card < n), RelSignature.RelStructure.fixingAlgebra A

theorem RelSignature.RelStructure.lowerRankAlgebra_le {S : RelSignature} (n : ℕ) : lowerRankAlgebra n ≤ inferInstance

theorem RelSignature.RelStructure.fixingAlgebra_le_lowerRankAlgebra {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (h : A.card < n) : fixingAlgebra A ≤ lowerRankAlgebra n

Each low-rank fixing algebra sits inside the conditioning factor.

theorem RelSignature.RelStructure.lowerRankAlgebra_mono {S : RelSignature} : Monotone lowerRankAlgebra

Monotone in the rank bound: a larger bound admits more generators.

theorem RelSignature.RelStructure.lowerRankAlgebra_zero {S : RelSignature} : lowerRankAlgebra 0 = ⊥

At rank bound 0 there are no generators.

theorem RelSignature.RelStructure.lowerRankAlgebra_one {S : RelSignature} : lowerRankAlgebra 1 = invariantAlgebra

At rank bound 1 the only generator is the empty set, so the conditioning factor is the invariant σ-algebra — the factor that carries whatever global information the law has. This is the base of the recursion, and the reason no NoNullary hypothesis is needed.

Invariance under relabeling

theorem RelSignature.RelStructure.comap_relabel_lowerRankAlgebra {S : RelSignature} [Fintype S.Srt] (σ : S.Srt → Equiv.Perm ℕ) (n : ℕ) : MeasurableSpace.comap (relabel σ) (lowerRankAlgebra n) = lowerRankAlgebra n

The conditioning factor is relabeling invariant, for an arbitrary sortwise permutation family under finitely many sorts — not merely a finitely supported one.

The generality is essential rather than cosmetic. Relabelings that displace infinitely many vertices arise naturally in the polling arguments this factor is built for — a map that shifts a block at every slot is not finitely supported — and the finite-support transport is simply unavailable for them. Since the proof needs nothing beyond each σ s being an Equiv, the hypothesis should not be narrowed.

Any such relabeling permutes the vertex sets of each rank, so it permutes the generators of lowerRankAlgebra n among themselves.

The rank bridge

theorem RelSignature.card_inter_lt_of_ne {S : RelSignature} {A A₀ : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) (hA₀ : A₀.card = n) (hne : A ≠ A₀) : (A ∩ A₀).card < n

Distinct supports of the same rank meet in lower rank. This is the exact bridge into lowerRankAlgebra: in the peel argument every C_A = A ∩ A₀ is a generator of the conditioning factor, because A and A₀ are distinct sets of the same cardinality.