Conditional independence of the fixing σ-algebras (R4 converse piece 2b, #107)

The relative-independence core of the converse representation theorem, following Austin, On exchangeable random variables and the statistics of large graphs and hypergraphs (Probab. Surveys 2008, arXiv:0801.1698), Lemma 3.11 and Proposition 3.12 (pp. 107–108), whose mechanism is the L² "tail property" squeeze of the proof of Theorem 3.1 (p. 99); the closest Kallenberg precursor is Lemma 7.6 (Probabilistic Symmetries, pp. 308–322). Target (public, final layer): for every exchangeable law M — no dissociation —

CondIndep (fixingAlgebra (A ∩ B)) (fixingAlgebra A) (fixingAlgebra B) (fixingAlgebra_le _) M.law.

This first layer is the measure-theoretic engine, all private:

• the L² squeeze condExp_ae_eq_condExp_of_integral_sq_le: nested conditioning algebras whose conditional expectations have comparable energies produce equal conditional expectations (Pythagoras for the projections);
• transport condExp_comp_of_measurePreserving: conditional expectation commutes with a measure-preserving map along MeasurableSpace.comap;
• the tail-property engine condExp_ae_eq_condExp_of_comap_eq combining the two: if a measure-preserving T fixes f a.e. and pulls the conditioning algebra m₁ back to a sub-algebra m₂ ≤ m₁, then μ[f|m₁] =ᵐ[μ] μ[f|m₂] — Austin's Theorem 3.1 step, abstracted.

No completion and no law enter any definition here. On top of the engine sit the a.e. invariance of fixingAlgebra A-events under every sortwise permutation fixing A (relabel_preimage_ae_eq_of_fixingAlgebra, the f ∘ T =ᵐ f input), and the poll geometry the engine runs on:

• pollIndex / pollShift — poll slots along a two-sided ℤ-orbit transported to ℕ. The two-sidedness is forced: a unilateral shift of the blocks is not a bijection (slot 0 would have no preimage), so the negative half serves as predecessor reservoir;
• pollBlock / pollPerm — the copies Q m of D = B \ A in slot m (with Q 0 = D) and the sortwise permutation that carries Q m onto Q (m+1) while fixing every vertex below the layout bound outside D, in particular all of A;
• pollTailAlgebra — the tail joins 𝒯 n = ⨆_{m ≥ n} fixingAlgebra (C ∪ Q m), with C = A ∩ B. The individual fixingAlgebra (C ∪ Q m) are not usable: over distinct deep blocks they are pairwise incomparable (hence no antitone sequence for Lévy downward), and fixingAlgebra (C ∪ Q m) ≤ fixingAlgebra B is false — monotonicity would demand C ∪ Q m ⊆ B, while Q m lies outside B. The joins are antitone, dominate fixingAlgebra B at n = 0, satisfy comap (relabel ρ) (𝒯 n) = 𝒯 (n+1) exactly, and have ⨅ n, 𝒯 n = fixingAlgebra C — the last a raw σ-algebra equality, no law and no null sets, available because the generators are fixing algebras rather than coordinate-generated window algebras (an earlier draft of this file carried such window algebras; the join route makes them unnecessary, so they are gone).

The layer closes with the reduction condExp_fixingAlgebra_ae_eq_condExp_inter: μ[f|fixingAlgebra B] =ᵐ μ[f|fixingAlgebra (A ∩ B)] for f a.e. invariant under the permutations fixing A, and its indicator form for a fixingAlgebra A-event. This is the (⋆) half of Austin's Proposition 3.12; the conditional-independence assembly is the next layer.

The poll blocks, the poll shift, and the tail joins

Invariance under a single permutation

The tail joins of the poll factors

The core reduction: conditioning on 𝓕 B collapses to 𝓕 (A ∩ B)

The conditional-independence theorem

theorem RelSignature.InfiniteRelExchangeableLaw.condIndep_fixingAlgebra {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) (A B : Finset ((s : S.Srt) × S.Vinfinite s)) : ProbabilityTheory.CondIndep (RelStructure.fixingAlgebra (A ∩ B)) (RelStructure.fixingAlgebra A) (RelStructure.fixingAlgebra B) ⋯ ↑M.law

Conditional independence of the fixing σ-algebras over their intersection (Austin, On exchangeable random variables and the statistics of large graphs and hypergraphs, Probab. Surveys 2008, arXiv:0801.1698, Lemma 3.11 and Proposition 3.12, pp. 107–108; Kallenberg, Probabilistic Symmetries and Invariance Principles, Lemma 7.6, p. 308 — the closest precursor there; Lemmas 7.18–7.19 belong to the later realization recursion, not to this statement):

for every exchangeable law M — no dissociation — the fixing σ-algebras of two finite tagged vertex sets are conditionally independent given the fixing σ-algebra of their intersection.

The relativized fixingAlgebra ∅ = invariantAlgebra carries whatever global information the law has (which is why no NoNullary hypothesis appears, and why dissociation is not needed: under a dissociated law the conditioning factor at A ∩ B = ∅ is trivial, but that is a consequence, not an assumption). At A = B, and likewise at A = ∅ or B = ∅, one outer algebra equals the conditioning algebra and the statement is tautological; the content is at disjoint nonempty A, B.

Proof: condIndep_iff reduces to a factorization of μ⟦E₁ ∩ E₂ | 𝓕 (A ∩ B)⟧ for E₁ ∈ 𝓕 A, E₂ ∈ 𝓕 B. Write 1_{E₁ ∩ E₂} = 1_{E₁} · 1_{E₂}, tower from 𝓕 (A ∩ B) through 𝓕 B, pull the 𝓕 B-measurable 1_{E₂} out, replace E[1_{E₁} | 𝓕 B] by E[1_{E₁} | 𝓕 (A ∩ B)] using the polled reduction condExp_indicator_fixingAlgebra_ae_eq_condExp_inter, and pull that 𝓕 (A ∩ B)-measurable factor out.