Boundary and exact layers of the coherent factors (R4 converse piece 3, #107)

The factor at a finite tagged vertex set A splits by anchor, into the coordinates carried over from proper subsets of A and the coordinates whose anchor is exactly A:

• BoundaryIndex A — indices whose anchor is a proper subset of A;
• ExactIndex A — the exact-anchor layer: indices whose anchor is exactly A;
• FactorSpace A ≃ᵐ BoundarySpace A × ExactSpace A.

This is a partition of coordinates by anchor, not of information. Anchors are not minimal: a Boolean expression can carry anchor A while naming an event that is already measurable over a proper subset — the seeds at A live in fixingAlgebra A, which contains fixingAlgebra C for every C ⊆ A. So the exact-anchor layer is not "the new information at A", and nothing in the splitting alone rules out redundancy between layers.

Why this decomposition

The recursion that builds the representing kernels is by |A|, with one kernel per finite A, conditioned on the whole proper-subset boundary at once. The two obvious alternatives are both wrong:

• Kernels for every pair C ⊆ A are redundant, and would force compatibility conditions between different versions of conditional distributions — each only defined a.e.
• A linear chain over some enumeration introduces an arbitrary ordering, and lets the value at A depend on sets incomparable to A, which violates the subset-locality of the Aldous–Hoover–Kallenberg formula.

Sampling only ExactSpace A, rather than resampling all of FactorSpace A, means the recursion never overwrites coordinate slots already generated at proper subsets — that much is structural, from the coordinate partition. Consistency with lower-anchor events that an exact-anchor coordinate happens to duplicate semantically is a different matter: it is an almost-sure/support property of stepKernel, which conditions on the boundary, and not something the partition delivers on its own.

Contents

• the boundary/exact index and space splitting, with factorSpaceProdEquiv;
• factorLaw, boundaryLaw, and exactLaw — the pushforwards of the law along the corresponding maps, with boundaryLaw_eq_map and exactLaw_eq_map identifying the latter two as the marginals of the first;
• factorLaw_map_factorProjection — projection consistency;
• factorLaw_map_factorSpaceEquiv — relabeling invariance, from exchangeability of the law.

The conditional kernel of the exact layer given the boundary is the next step, and is where the standard Borel structure of these spaces is used.

The boundary and exact layers

def RelSignature.CoherentBasis.BoundaryIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u

Indices whose anchor is a proper subset of A: the coordinates at A carried over from strictly smaller vertex sets.

Equations

• B.BoundaryIndex A = { i : B.ι // B.anchor i ⊂ A }

def RelSignature.CoherentBasis.ExactIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u

The exact-anchor layer: indices whose anchor is exactly A.

Note that this is an anchor condition, not a minimality condition — an expression anchored at A may still name an event measurable over a proper subset, since fixingAlgebra C ≤ fixingAlgebra A for C ⊆ A. The layer is disjoint from the boundary layer as a set of coordinates; semantic non-redundancy is not claimed here.

Equations

• B.ExactIndex A = { i : B.ι // B.anchor i = A }

instance RelSignature.CoherentBasis.instCountableBoundaryIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Countable (B.BoundaryIndex A)

instance RelSignature.CoherentBasis.instCountableExactIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Countable (B.ExactIndex A)

@[reducible, inline]

abbrev RelSignature.CoherentBasis.BoundarySpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u

The boundary layer of the factor space.

Equations

• B.BoundarySpace A = (B.BoundaryIndex A → Bool)

@[reducible, inline]

abbrev RelSignature.CoherentBasis.ExactSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u

The exact layer of the factor space.

Equations

• B.ExactSpace A = (B.ExactIndex A → Bool)

instance RelSignature.CoherentBasis.instStandardBorelSpaceBoundarySpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : StandardBorelSpace (B.BoundarySpace A)

instance RelSignature.CoherentBasis.instStandardBorelSpaceExactSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : StandardBorelSpace (B.ExactSpace A)

noncomputable def RelSignature.CoherentBasis.factorSpaceProdEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.FactorSpace A ≃ᵐ B.BoundarySpace A × B.ExactSpace A

The factor space splits as boundary times exact: an index anchored inside A is anchored either properly inside it or exactly at it, and never both.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RelSignature.CoherentBasis.boundaryMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : S.RelStructure S.Vinfinite → B.BoundarySpace A

The boundary half of the factor map.

Equations

• B.boundaryMap A X = ((B.factorSpaceProdEquiv A) (B.factorMap A X)).1

noncomputable def RelSignature.CoherentBasis.exactMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : S.RelStructure S.Vinfinite → B.ExactSpace A

The exact half of the factor map.

Equations

• B.exactMap A X = ((B.factorSpaceProdEquiv A) (B.factorMap A X)).2

theorem RelSignature.CoherentBasis.measurable_boundaryMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Measurable (B.boundaryMap A)

theorem RelSignature.CoherentBasis.measurable_exactMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Measurable (B.exactMap A)

theorem RelSignature.CoherentBasis.measurable_exactMap_fixingAlgebra {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Measurable (B.exactMap A)

The exact-anchor layer at A is measurable for fixingAlgebra A, not merely for the ambient algebra. General factor API rather than a rank-one fact: any argument that bundles exact-layer events over a support needs this sharpening of measurable_exactMap.

Relabeling the two layers

theorem RelSignature.CoherentBasis.image_ssubset_image {S : RelSignature} (σ : ↥S.FinSuppPerm) {s t : Finset ((s : S.Srt) × S.Vinfinite s)} (h : s ⊂ t) : Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) s ⊂ Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) t

Relabeling is strictly monotone on vertex sets: it preserves proper inclusion, because image_image_inv recovers the source.

noncomputable def RelSignature.CoherentBasis.boundaryIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.BoundaryIndex A ≃ B.BoundaryIndex (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)

The relabeling equivalence restricted to the boundary layer.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RelSignature.CoherentBasis.exactIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.ExactIndex A ≃ B.ExactIndex (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)

The relabeling equivalence restricted to the exact-anchor layer.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RelSignature.CoherentBasis.boundarySpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.BoundarySpace (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A) ≃ᵐ B.BoundarySpace A

The boundary layer as a measurable equivalence, oriented like factorSpaceEquiv: image-set space to original-set space.

Equations

• B.boundarySpaceEquiv σ A = { toEquiv := (B.boundaryIndexEquiv σ A).symm.arrowCongr (Equiv.refl Bool), measurable_toFun := ⋯, measurable_invFun := ⋯ }

noncomputable def RelSignature.CoherentBasis.exactSpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.ExactSpace (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A) ≃ᵐ B.ExactSpace A

The exact-anchor layer as a measurable equivalence, same orientation.

Equations

• B.exactSpaceEquiv σ A = { toEquiv := (B.exactIndexEquiv σ A).symm.arrowCongr (Equiv.refl Bool), measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem RelSignature.CoherentBasis.prodMap_comp_factorSpaceProdEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Prod.map ⇑(B.boundarySpaceEquiv σ A) ⇑(B.exactSpaceEquiv σ A) ∘ ⇑(B.factorSpaceProdEquiv (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)) = ⇑(B.factorSpaceProdEquiv A) ∘ ⇑(B.factorSpaceEquiv σ A)

The splitting is equivariant: relabeling and then splitting is splitting and then relabeling each layer. Definitional — both routes act by σ and differ only in which containment proof is carried.

theorem RelSignature.CoherentBasis.boundarySpaceEquiv_comp_boundaryMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : ⇑(B.boundarySpaceEquiv σ A) ∘ B.boundaryMap (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A) = B.boundaryMap A ∘ RelStructure.relabel ↑σ

The boundary map is equivariant, through the layer equivalence.

theorem RelSignature.CoherentBasis.exactSpaceEquiv_comp_exactMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : ⇑(B.exactSpaceEquiv σ A) ∘ B.exactMap (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A) = B.exactMap A ∘ RelStructure.relabel ↑σ

The exact-anchor map is equivariant, through the layer equivalence.

The factor laws

noncomputable def RelSignature.CoherentBasis.factorLaw {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.Measure (B.FactorSpace A)

The factor law at A: the law of the factor map under M.

Equations

• B.factorLaw A = MeasureTheory.Measure.map (B.factorMap A) ↑M.law

noncomputable def RelSignature.CoherentBasis.boundaryLaw {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.Measure (B.BoundarySpace A)

The boundary law at A — the conditioning measure of the step kernel.

Equations

• B.boundaryLaw A = MeasureTheory.Measure.map (B.boundaryMap A) ↑M.law

noncomputable def RelSignature.CoherentBasis.exactLaw {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.Measure (B.ExactSpace A)

The exact law at A.

Equations

• B.exactLaw A = MeasureTheory.Measure.map (B.exactMap A) ↑M.law

instance RelSignature.CoherentBasis.instIsProbabilityMeasureFactorSpaceFactorLaw {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.IsProbabilityMeasure (B.factorLaw A)

instance RelSignature.CoherentBasis.instIsProbabilityMeasureBoundarySpaceBoundaryLaw {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.IsProbabilityMeasure (B.boundaryLaw A)

instance RelSignature.CoherentBasis.instIsProbabilityMeasureExactSpaceExactLaw {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.IsProbabilityMeasure (B.exactLaw A)

theorem RelSignature.CoherentBasis.boundaryLaw_eq_map {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.boundaryLaw A = MeasureTheory.Measure.map (fun (p : B.FactorSpace A) => ((B.factorSpaceProdEquiv A) p).1) (B.factorLaw A)

The boundary law is a marginal of the factor law, through the product decomposition.

theorem RelSignature.CoherentBasis.exactLaw_eq_map {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.exactLaw A = MeasureTheory.Measure.map (fun (p : B.FactorSpace A) => ((B.factorSpaceProdEquiv A) p).2) (B.factorLaw A)

The exact law is the other marginal of the factor law, symmetric to boundaryLaw_eq_map. Used when checking that stepKernel disintegrates the factor law.

theorem RelSignature.CoherentBasis.factorLaw_map_factorProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {C A : Finset ((s : S.Srt) × S.Vinfinite s)} (hCA : C ⊆ A) : MeasureTheory.Measure.map (B.factorProjection hCA) (B.factorLaw A) = B.factorLaw C

Projection consistency: the factor laws are compatible along the sub-index inclusions. Immediate, since factorProjection_factorMap is rfl.

theorem RelSignature.CoherentBasis.boundaryLaw_map_boundarySpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.Measure.map (⇑(B.boundarySpaceEquiv σ A)) (B.boundaryLaw (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)) = B.boundaryLaw A

Relabeling invariance of the boundary law. Public API: otherwise it gets rederived at each use in the recursion.

theorem RelSignature.CoherentBasis.exactLaw_map_exactSpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.Measure.map (⇑(B.exactSpaceEquiv σ A)) (B.exactLaw (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)) = B.exactLaw A

Relabeling invariance of the exact law, likewise.

theorem RelSignature.CoherentBasis.factorLaw_map_factorSpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasureTheory.Measure.map (⇑(B.factorSpaceEquiv σ A)) (B.factorLaw (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)) = B.factorLaw A

Relabeling invariance of the factor laws: transporting the factor law at the image vertex set along factorSpaceEquiv returns the factor law at A. This is where exchangeability of M enters — everything before it was law-free.