The singleton peel (R4 converse piece 3, #107) #
Mutual conditional independence at rank one, for any vertex-indexed family whose members are measurable for their own singleton fixing algebra.
The argument never mentions a coherent basis, a factor map, or any particular reading of the
structure. It depends on one thing only: distinct singletons are disjoint, so the two-set theorem
InfiniteRelExchangeableLaw.condIndep_fixingAlgebra conditions on
fixingAlgebra ∅ = invariantAlgebra at every stage of the peel, and the conditioning algebra
never moves.
Why this is the right level of generality #
Both consumers are instances: the coherent-basis exact layers exactMap {v}, and the raw
relation blocks blockMap {v}. Neither is more fundamental, and phrasing the peel against either
would force the other to be obtained by a transfer lemma that does not exist. The hypothesis
Measurable[fixingAlgebra {v}] (Y v) is exactly what the argument consumes.
This module also carries the raw-block instance, so that Graphon.RelRankRepresentation stays
interface-only: the specification must not depend on the conditional-independence proof layer.
Where it stops #
Above rank one the peel fails, and not for a technical reason. Distinct supports of equal rank
can meet — card_inter_lt_of_ne gives only that they meet in strictly lower rank — so a stage
of the peel would condition on fixingAlgebra of a nonempty intersection, a strictly larger
algebra. Conditional independence is not preserved under enlarging the conditioning, so the
stages no longer compose.
The block at A is measurable for fixingAlgebra A. Every tagged value occurring in a
coordinate of support A lies in A, so a relabeling fixing A pointwise fixes the coordinate
itself — no null sets, and no reference to any basis.
The singleton peel. A vertex-indexed family, each member measurable for the fixing algebra
of its own vertex, is mutually conditionally independent given the invariant σ-algebra — for
an arbitrary exchangeable law, with no dissociation and no NoNullary.
Stated over the whole vertex index rather than a fixed finite family: iCondIndepFun already
quantifies over finite subfamilies.
Mutual conditional independence of the raw singleton blocks given the invariant σ-algebra, for an arbitrary exchangeable law. An instance of the peel above, phrased entirely in raw relation coordinates — no coherent basis appears.