The five-way extremality equivalence for exchangeable relational laws (R3c, #106)

The honest, representation-free five-way characterization: for an exchangeable law on the infinite structure space of a finite-sort signature,

dissociated ↔ restriction-independent ↔ vertex-tail-trivial ↔ ergodic ↔ extreme point of the invariant probability simplex,

assembled from the R3a block machinery, the R3b triangle (closed by Lévy's downward theorem), the R3c ergodicity links, and the ported ergodic ↔ extreme-point theorem. No functional-AHK or mixing-representation input anywhere in the proof graph; the Dirac-mixing description of the extreme laws is a later corollary of R5.

The directed specialization (digraphSig) is exercised as a regression test: the generic equivalence applies verbatim to InfiniteExchangeableDigraphLaw.

theorem RelSignature.tfae_extremality {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) : [M.IsDissociated, M.RestrictionIndependent, M.VertexTailTrivial, M.IsErgodic, ↑M.law ∈ Set.extremePoints ENNReal S.invariantProbabilityMeasures].TFAE

The five-way extremality equivalence (R3c): dissociation, restriction independence, vertex-tail triviality, ergodicity under the finitely supported relabelings, and genuine extremality in the invariant probability simplex all coincide.

theorem RelSignature.isDissociated_iff_mem_extremePoints {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) : M.IsDissociated ↔ ↑M.law ∈ Set.extremePoints ENNReal S.invariantProbabilityMeasures

Extremality ↔ dissociation, the endpoint pairing of the five-way equivalence.

Directed regression test (the digraphSig specialization)