Restriction independence and vertex-tail triviality (AHK umbrella, R3b / #106)

The generic equivalence between dissociation and restriction independence, and the implication to vertex-tail triviality, for exchangeable relational laws:

• InfiniteRelExchangeableLaw.RestrictionIndependent — for every block size the initial and after-block σ-algebras are independent;

• InfiniteRelExchangeableLaw.VertexTailTrivial — every vertex-tail event has law-measure 0 or 1;

• isDissociated_iff_restrictionIndependent — dissociation ↔ restriction independence: independence of the comap σ-algebras of the two block maps is the block-pair map factorization (IndepFun_iff_Indep + indepFun_iff_map_prod_eq_prod_map_map), and the finite tail windows exhaust the after-block σ-algebra (R3a);

• RestrictionIndependent.vertexTailTrivial — a vertex-tail event is independent of every initial σ-algebra, hence (the initial σ-algebras generating, R3a) of itself.

• VertexTailTrivial.isDissociated / isDissociated_iff_vertexTailTrivial — the closing arrow, representation-free: condition the initial-event indicator on successively later diagonal tail algebras; Lévy's downward theorem (Graphon/LevyDownward.lean) converges the conditional expectations to the vertex-tail one, which tail triviality makes a.e. constant; exchangeability keeps the joint mass with an arbitrarily far window constant (law_map_restrict_pair); in the limit the block mass factorizes exactly. (The undirected proof instead rides the graphon mixture representation; the generic theory keeps the characterization representation-free, with R5's Dirac-mixing as a later corollary.)

Window monotonicity

theorem RelSignature.RelStructure.tailWindowAlgebra_mono {S : RelSignature} (k : S.Srt → ℕ) {l l' : S.Srt → ℕ} (h : ∀ (s : S.Srt), l s ≤ l' s) : tailWindowAlgebra k l ≤ tailWindowAlgebra k l'

The finite tail windows are monotone in the window size.

theorem RelSignature.RelStructure.tailWindowAlgebra_le_tailAlgebra {S : RelSignature} (k l : S.Srt → ℕ) : tailWindowAlgebra k l ≤ tailAlgebra k

The two properties

def RelSignature.InfiniteRelExchangeableLaw.RestrictionIndependent {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : Prop

Restriction independence: for every block size, the structure on the initial block is independent of the structure on the remaining vertices.

Equations

• M.RestrictionIndependent = ∀ (k : S.Srt → ℕ), ProbabilityTheory.Indep (RelSignature.RelStructure.initialAlgebra k) (RelSignature.RelStructure.tailAlgebra k) ↑M.law

def RelSignature.InfiniteRelExchangeableLaw.VertexTailTrivial {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : Prop

Vertex-tail triviality: every vertex-tail event has law-measure 0 or 1.

Equations

• M.VertexTailTrivial = ∀ (s : Set (S.RelStructure S.Vinfinite)), MeasurableSet s → ↑M.law s = 0 ∨ ↑M.law s = 1

Dissociation ↔ restriction independence

theorem RelSignature.InfiniteRelExchangeableLaw.IsDissociated.indep_initial_tailWindow {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (hM : M.IsDissociated) (k l : S.Srt → ℕ) : ProbabilityTheory.Indep (RelStructure.initialAlgebra k) (RelStructure.tailWindowAlgebra k l) ↑M.law

Finite-window independence from dissociation: comap-σ-algebra independence of the initial block and a tail window is exactly the block-pair map factorization.

theorem RelSignature.InfiniteRelExchangeableLaw.IsDissociated.restrictionIndependent {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (hM : M.IsDissociated) : M.RestrictionIndependent

Dissociation implies restriction independence: the finite windows exhaust the after-block σ-algebra.

theorem RelSignature.InfiniteRelExchangeableLaw.RestrictionIndependent.isDissociated {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (hM : M.RestrictionIndependent) : M.IsDissociated

Restriction independence implies dissociation: restrict the independence to a window and read it as the block-pair map factorization.

theorem RelSignature.isDissociated_iff_restrictionIndependent {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : M.IsDissociated ↔ M.RestrictionIndependent

Dissociation ↔ restriction independence (R3b).

Restriction independence implies vertex-tail triviality

theorem RelSignature.InfiniteRelExchangeableLaw.RestrictionIndependent.vertexTailTrivial {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (hM : M.RestrictionIndependent) : M.VertexTailTrivial

Restriction independence implies vertex-tail triviality: a vertex-tail event is independent of every initial σ-algebra, hence — the initial σ-algebras generating the Borel σ-algebra — independent of itself.

theorem RelSignature.InfiniteRelExchangeableLaw.IsDissociated.vertexTailTrivial {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (hM : M.IsDissociated) : M.VertexTailTrivial

Dissociation implies vertex-tail triviality (R3b chain).

Vertex-tail triviality implies dissociation (the closing arrow)

theorem RelSignature.InfiniteRelExchangeableLaw.VertexTailTrivial.isDissociated {S : RelSignature} [Fintype S.Srt] {M : S.InfiniteRelExchangeableLaw} (hM : M.VertexTailTrivial) : M.IsDissociated

Vertex-tail triviality implies dissociation (representation-free): condition the initial-event indicator on successively later diagonal tail algebras; Lévy's downward theorem converges the conditional expectations to the vertex-tail one, which tail triviality makes a.e. constant; exchangeability keeps the joint mass with an arbitrarily far window constant; in the limit the block mass factorizes exactly.

theorem RelSignature.isDissociated_iff_vertexTailTrivial {S : RelSignature} [Fintype S.Srt] (M : S.InfiniteRelExchangeableLaw) : M.IsDissociated ↔ M.VertexTailTrivial

Dissociation ↔ vertex-tail triviality (R3b complete, representation-free).