The rank successor decomposition (R4 converse piece 3, #107)

Unit 1 of the rank transition n → n+1: the structural splitting of the lower-rank factor space into everything below rank n and the layer at rank exactly n. Law-free throughout — this file defines index types, equivalences and projections, and mentions no measure.

The layer is a Bool-cube, not a dependent product

The layer at rank n is naturally indexed by supports of cardinality n, one ExactSpace A per support, so the obvious definition is the dependent product Π A : RankSupport S n, ExactSpace A. That definition would be a mistake. It forces every downstream conditional law to be a kernel into a dependent product, and Mathlib has no countable dependent product of kernels — there is no Kernel.pi; the only Π-valued kernels are the Ionescu–Tulcea trajectory kernels, which are ℕ-indexed chains whose source is the history rather than a fixed common parameter.

Since ExactSpace A = ExactIndex A → Bool, the dependent product is already a Bool-cube:

Π A : RankSupport S n, ExactSpace A ≃ ((Σ A, ExactIndex A) → Bool)

and the sigma index is just {i // (anchor i).card = n}. So the layer is defined directly as that Bool-cube (RankLayerIndex / RankLayerSpace), with sigmaExactIndexEquiv recording the bridge and rankLayerMap_sigmaExactIndexEquiv identifying each block with exactMap A. Countability and standard Borelness are then the same instances that already serve LowerFactorSpace, and no product kernel is needed anywhere downstream: a conditional law of the whole layer is an ordinary condDistrib into a standard Borel space, and mutual conditional independence supplies the finite products that finite-cylinder extensionality consumes.

Contents

• RankLayerIndex / RankLayerSpace / rankLayerMap — the layer at rank exactly n;
• RelSignature.RankSupport and sigmaExactIndexEquiv — the bridge to the per-support view;
• lowerIndexSuccEquiv and lowerFactorSpaceSuccEquiv — the successor split LowerFactorSpace (n+1) ≃ᵐ LowerFactorSpace n × RankLayerSpace n;
• lowerToBoundaryProjection — for A.card = n, the rank-n factor reads the boundary at A, with lowerToBoundaryProjection_lowerFactorMap definitional;
• rankSupportEquiv / rankLayerIndexEquiv / rankLayerSpaceEquiv — the relabeling actions, with lowerIndexSuccEquiv_rankLayerIndexEquiv the square against the successor split.

The successor split is a case distinction on card < n versus card = n, so it is a dite and the index-level square against it, lowerIndexSuccEquiv_rankLayerIndexEquiv, is not definitional: the branch conditions on the two sides agree only after rewriting anchor cardinality through the image map. The named coordinate and projection compatibility lemmas are definitional — rankLayerMap_sigmaExactIndexEquiv, lowerFactorSpaceSuccEquiv_lowerFactorMap, fst_lowerFactorSpaceSuccEquiv, lowerToBoundaryProjection_lowerFactorMap, rankLayerToExactProjection_rankLayerMap, the three naturality squares, and the space-level successor square lowerFactorSpaceSuccEquiv_lowerFactorSpaceEquiv, which escapes the case split because it is built from lowerIndexSuccEquiv.symm and that is a Sum.elim.

def RelSignature.RankSupport (S : RelSignature) (n : ℕ) : Type u_1

The supports of rank exactly n: the index of the family whose layers make up the rank-n step. Not the index of the layer space itself — see the module header.

Equations

• S.RankSupport n = { A : Finset ((s : S.Srt) × S.Vinfinite s) // A.card = n }

instance RelSignature.instCountableRankSupportOfSrt {S : RelSignature} [Countable S.Srt] (n : ℕ) : Countable (S.RankSupport n)

theorem RelSignature.card_image_sigmaMap {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) (σ : ↥S.FinSuppPerm) : (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A).card = n

Relabeling preserves rank: the image map is injective, so it preserves anchor cardinality. The workhorse of every rank-indexed transport in this file.

noncomputable def RelSignature.rankSupportPerm {S : RelSignature} (σ : (s : S.Srt) → Equiv.Perm (S.Vinfinite s)) (n : ℕ) : S.RankSupport n ≃ S.RankSupport n

An arbitrary sortwise permutation permutes the supports of each rank. Finite support is irrelevant here: only injectivity is used, and that is what preserves cardinality. Stated for arbitrary sortwise permutations because the exchangeability of a law is an invariance under all of them, not only the finitely supported ones.

Equations

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

@[simp]

theorem RelSignature.rankSupportPerm_coe {S : RelSignature} (σ : (s : S.Srt) → Equiv.Perm (S.Vinfinite s)) (n : ℕ) (A : S.RankSupport n) : ↑((rankSupportPerm σ n) A) = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(σ s)) ↑A

theorem RelSignature.mem_rankSupportPerm {S : RelSignature} (σ : (s : S.Srt) → Equiv.Perm (S.Vinfinite s)) (n : ℕ) (A : S.RankSupport n) (v : (s : S.Srt) × S.Vinfinite s) : v ∈ ↑((rankSupportPerm σ n) A) ↔ ∃ a ∈ ↑A, Sigma.map id (fun (s : S.Srt) => ⇑(σ s)) a = v

Membership in a permuted support, stated without an image so that no DecidableEq instance appears in the type. Consumers over a concrete carrier have a natural instance that is not definitionally the classical one used to form the image, and rankSupportPerm_coe is then unusable there; this form is not.

noncomputable def RelSignature.rankSupportEquiv {S : RelSignature} (σ : ↥S.FinSuppPerm) (n : ℕ) : S.RankSupport n ≃ S.RankSupport n

A relabeling permutes the supports of each rank — the finitely supported case.

Equations

• RelSignature.rankSupportEquiv σ n = RelSignature.rankSupportPerm (↑σ) n

@[simp]

theorem RelSignature.rankSupportEquiv_one {S : RelSignature} (n : ℕ) : rankSupportEquiv 1 n = Equiv.refl (S.RankSupport n)

@[simp]

theorem RelSignature.rankSupportEquiv_mul {S : RelSignature} (σ τ : ↥S.FinSuppPerm) (n : ℕ) : rankSupportEquiv (σ * τ) n = (rankSupportEquiv τ n).trans (rankSupportEquiv σ n)

The rank layer

def RelSignature.CoherentBasis.RankLayerIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Type u

Indices anchored at a support of cardinality exactly n.

Equations

• B.RankLayerIndex n = { i : B.ι // (B.anchor i).card = n }

instance RelSignature.CoherentBasis.instCountableRankLayerIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Countable (B.RankLayerIndex n)

@[reducible, inline]

abbrev RelSignature.CoherentBasis.RankLayerSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Type u

The rank-n layer of the factor space, as a Bool-cube on a countable index.

Equations

• B.RankLayerSpace n = (B.RankLayerIndex n → Bool)

instance RelSignature.CoherentBasis.instStandardBorelSpaceRankLayerSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : StandardBorelSpace (B.RankLayerSpace n)

noncomputable def RelSignature.CoherentBasis.rankLayerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : S.RelStructure S.Vinfinite → B.RankLayerSpace n

The rank-n layer map: evaluate every basis event anchored at rank exactly n.

Equations

• B.rankLayerMap n X i = decide (X ∈ B.event ↑i)

theorem RelSignature.CoherentBasis.measurable_rankLayerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : Measurable (B.rankLayerMap n)

The bridge to the per-support view

def RelSignature.CoherentBasis.sigmaExactIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : (A : S.RankSupport n) × B.ExactIndex ↑A ≃ B.RankLayerIndex n

The layer is the disjoint union of the exact layers over the supports of rank n. This is the bridge between the Bool-cube definition of RankLayerSpace and the per-support view in which the rank-n step is a family indexed by RankSupport S n.

Equations

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

theorem RelSignature.CoherentBasis.rankLayerMap_sigmaExactIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) (X : S.RelStructure S.Vinfinite) (A : S.RankSupport n) (i : B.ExactIndex ↑A) : B.rankLayerMap n X ((B.sigmaExactIndexEquiv n) ⟨A, i⟩) = B.exactMap (↑A) X i

Each block of the layer map is the exact-anchor map at its support. Definitional: both sides evaluate the same basis event at the same point.

The successor split

def RelSignature.CoherentBasis.lowerIndexSuccEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : B.LowerIndex (n + 1) ≃ B.LowerIndex n ⊕ B.RankLayerIndex n

Rank below n+1 means rank below n or rank exactly n.

Equations

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

noncomputable def RelSignature.CoherentBasis.lowerFactorSpaceSuccEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : B.LowerFactorSpace (n + 1) ≃ᵐ B.LowerFactorSpace n × B.RankLayerSpace n

The successor split of the lower-rank factor space: everything below rank n, together with the layer at rank exactly n.

Equations

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

theorem RelSignature.CoherentBasis.fst_lowerFactorSpaceSuccEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) (f : B.LowerFactorSpace (n + 1)) : ((B.lowerFactorSpaceSuccEquiv n) f).1 = B.lowerFactorProjection ⋯ f

The successor split refines the rank nesting: its first component is the rank-n projection.

theorem RelSignature.CoherentBasis.lowerFactorSpaceSuccEquiv_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) (X : S.RelStructure S.Vinfinite) : (B.lowerFactorSpaceSuccEquiv n) (B.lowerFactorMap (n + 1) X) = (B.lowerFactorMap n X, B.rankLayerMap n X)

The successor split applied to the factor map reads the two layers.

The boundary projection at a support of rank n

def RelSignature.CoherentBasis.boundaryToLowerIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : B.BoundaryIndex A → B.LowerIndex n

A boundary index at a support of rank n has rank < n.

Equations

• B.boundaryToLowerIndex hA i = ⟨↑i, ⋯⟩

def RelSignature.CoherentBasis.lowerToBoundaryProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : B.LowerFactorSpace n → B.BoundarySpace A

The rank-n factor reads the boundary at every support of rank n.

Equations

• B.lowerToBoundaryProjection hA f = f ∘ B.boundaryToLowerIndex hA

theorem RelSignature.CoherentBasis.measurable_lowerToBoundaryProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : Measurable (B.lowerToBoundaryProjection hA)

theorem RelSignature.CoherentBasis.lowerToBoundaryProjection_lowerFactorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : B.lowerToBoundaryProjection hA ∘ B.lowerFactorMap n = B.boundaryMap A

Definitional, as intended: the boundary map at A factors through the rank-n factor.

The exact projection at a support of rank n

def RelSignature.CoherentBasis.rankLayerToExactIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : B.ExactIndex A → B.RankLayerIndex n

An exact index at a support of rank n lies in the rank-n layer.

Equations

• B.rankLayerToExactIndex hA i = ⟨↑i, ⋯⟩

def RelSignature.CoherentBasis.rankLayerToExactProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : B.RankLayerSpace n → B.ExactSpace A

The layer projects onto the exact layer at each support of rank n. The per-support view of the Bool-cube: this is the map along which the layer's conditional law restricts to stepKernel A's target.

Equations

• B.rankLayerToExactProjection hA f = f ∘ B.rankLayerToExactIndex hA

theorem RelSignature.CoherentBasis.measurable_rankLayerToExactProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : Measurable (B.rankLayerToExactProjection hA)

theorem RelSignature.CoherentBasis.rankLayerToExactProjection_rankLayerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : B.rankLayerToExactProjection hA ∘ B.rankLayerMap n = B.exactMap A

Definitional: the exact-anchor map at A factors through the rank-n layer.

Relabeling actions

noncomputable def RelSignature.CoherentBasis.rankLayerIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : B.RankLayerIndex n ≃ B.RankLayerIndex n

A relabeling permutes the rank-n layer index: the action transports anchors by an injective image map, so it preserves cardinality exactly.

Equations

• B.rankLayerIndexEquiv σ n = { toFun := fun (i : B.RankLayerIndex n) => ⟨B.act σ ↑i, ⋯⟩, invFun := fun (j : B.RankLayerIndex n) => ⟨B.act σ⁻¹ ↑j, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem RelSignature.CoherentBasis.rankLayerIndexEquiv_apply_coe {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) (i : B.RankLayerIndex n) : ↑((B.rankLayerIndexEquiv σ n) i) = B.act σ ↑i

@[simp]

theorem RelSignature.CoherentBasis.rankLayerIndexEquiv_one {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : B.rankLayerIndexEquiv 1 n = Equiv.refl (B.RankLayerIndex n)

Identity, as an equality of equivalences: these are automorphisms of one fixed type.

@[simp]

theorem RelSignature.CoherentBasis.rankLayerIndexEquiv_mul {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ τ : ↥S.FinSuppPerm) (n : ℕ) : B.rankLayerIndexEquiv (σ * τ) n = (B.rankLayerIndexEquiv τ n).trans (B.rankLayerIndexEquiv σ n)

Composition, likewise.

theorem RelSignature.CoherentBasis.rankLayerMap_rankLayerIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) (X : S.RelStructure S.Vinfinite) (i : B.RankLayerIndex n) : B.rankLayerMap n X ((B.rankLayerIndexEquiv σ n) i) = B.rankLayerMap n (RelStructure.relabel (↑σ) X) i

Naturality of the layer map, with the same orientation as lowerFactorMap_lowerIndexEquiv — forced by event_act being a preimage equality.

noncomputable def RelSignature.CoherentBasis.rankLayerSpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : B.RankLayerSpace n ≃ᵐ B.RankLayerSpace n

A relabeling as a measurable automorphism of the layer space, by coordinate reindexing.

Equations

• B.rankLayerSpaceEquiv σ n = { toEquiv := (B.rankLayerIndexEquiv σ n).symm.arrowCongr (Equiv.refl Bool), measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem RelSignature.CoherentBasis.rankLayerSpaceEquiv_comp_rankLayerMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : ⇑(B.rankLayerSpaceEquiv σ n) ∘ B.rankLayerMap n = B.rankLayerMap n ∘ RelStructure.relabel ↑σ

theorem RelSignature.CoherentBasis.lowerIndexSuccEquiv_rankLayerIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : ⇑(B.lowerIndexSuccEquiv n) ∘ ⇑(B.lowerIndexEquiv σ (n + 1)) = Sum.map ⇑(B.lowerIndexEquiv σ n) ⇑(B.rankLayerIndexEquiv σ n) ∘ ⇑(B.lowerIndexSuccEquiv n)

The successor split is equivariant. Not definitional: the split branches on card < n, and the two sides' branch conditions agree only after transporting anchor cardinality through the image map — which is exactly rankLayerIndexEquiv's defining computation.

@[simp]

theorem RelSignature.CoherentBasis.rankLayerSpaceEquiv_apply {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) (g : B.RankLayerSpace n) (i : B.RankLayerIndex n) : (B.rankLayerSpaceEquiv σ n) g i = g ((B.rankLayerIndexEquiv σ n) i)

@[simp]

theorem RelSignature.CoherentBasis.rankLayerSpaceEquiv_one {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (n : ℕ) : B.rankLayerSpaceEquiv 1 n = MeasurableEquiv.refl (B.RankLayerSpace n)

Identity, as an equality of measurable equivalences.

@[simp]

theorem RelSignature.CoherentBasis.rankLayerSpaceEquiv_mul {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ τ : ↥S.FinSuppPerm) (n : ℕ) : B.rankLayerSpaceEquiv (σ * τ) n = (B.rankLayerSpaceEquiv σ n).trans (B.rankLayerSpaceEquiv τ n)

Composition, contravariantly, matching lowerFactorSpaceEquiv_mul.

Naturality

theorem RelSignature.CoherentBasis.rankLayerIndexEquiv_sigmaExactIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) (A : S.RankSupport n) (i : B.ExactIndex ↑A) : (B.rankLayerIndexEquiv σ n) ((B.sigmaExactIndexEquiv n) ⟨A, i⟩) = (B.sigmaExactIndexEquiv n) ⟨(rankSupportEquiv σ n) A, (B.exactIndexEquiv σ ↑A) i⟩

The support/exact bridge is natural: acting on a support and its exact index agrees with acting on the corresponding layer index. Definitional — both routes are act σ on the index and differ only in which anchor proof is carried.

theorem RelSignature.CoherentBasis.exactSpaceEquiv_rankLayerToExactProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : ⇑(B.exactSpaceEquiv σ A) ∘ B.rankLayerToExactProjection ⋯ = B.rankLayerToExactProjection hA ∘ ⇑(B.rankLayerSpaceEquiv σ n)

The exact projection is natural. Reading the exact layer at A after relabeling is relabeling after reading it at the image support. Definitional.

theorem RelSignature.CoherentBasis.boundarySpaceEquiv_lowerToBoundaryProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) : ⇑(B.boundarySpaceEquiv σ A) ∘ B.lowerToBoundaryProjection ⋯ = B.lowerToBoundaryProjection hA ∘ ⇑(B.lowerFactorSpaceEquiv σ n)

The boundary projection is natural, likewise definitional.

theorem RelSignature.CoherentBasis.lowerFactorSpaceSuccEquiv_lowerFactorSpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (n : ℕ) : ⇑(B.lowerFactorSpaceSuccEquiv n) ∘ ⇑(B.lowerFactorSpaceEquiv σ (n + 1)) = Prod.map ⇑(B.lowerFactorSpaceEquiv σ n) ⇑(B.rankLayerSpaceEquiv σ n) ∘ ⇑(B.lowerFactorSpaceSuccEquiv n)

The successor split is equivariant at the level of spaces — and here, unlike the index-level square lowerIndexSuccEquiv_rankLayerIndexEquiv, the statement is definitional. The space-level map is built from lowerIndexSuccEquiv.symm, which is a Sum.elim and so computes on the constructors; the forward dite that forces the case split never appears.