The rank-one representation exists (R4 converse piece 3, #107)

Every exchangeable law has a rank-one RankRepresentation. The base case of the coupled rank recursion, assembled from the five step-3 units. No dissociation, no NoNullary, and no basis in the statement: a coherent basis is chosen inside the proof (nonempty_coherentBasis) and never escapes.

The fields, by provenance:

• the coupling and its marginals, probability, and joint relabeling invariance are the transported #161 coupling (exists_rankOneLatentCoupling);
• lower_recovers is the nullary-block recovery (exists_blockMap_recovery_of_card_lt_one);
• screening is the per-support specialization (condIndepFun_blockMap_restObservation_one) of the conditioning ladder (iCondIndepFun_blockMap_singleton_comap_snd), fed by the coupling's conditional-independence clause at the identity reading.

Everything conditional is modulo the coupling measure. In particular no identification of the invariant σ-algebra with the σ-algebra of the latent is asserted — the latent resolves the rank-one factor and is conditionally independent of everything else, which is strictly weaker and is all the recursion consumes.

theorem RelSignature.InfiniteRelExchangeableLaw.nonempty_rankRepresentation_one {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) : Nonempty (M.RankRepresentation 1)

The rank-one representation exists, for an arbitrary exchangeable law: a coupling of the law with the rank-one latents satisfying all RankRepresentation clauses — marginals, joint relabeling invariance, local recovery of everything below rank one, and rank-truncated local screening at every rank-one support.