The joint representation interface (R4 converse piece 3, #107)

The specification a rank-n representation must satisfy. Interface only: no existence theorem is proved or claimed here, at any rank.

Why the primitive is a coupling

The previous design took a map RankLatentSpace n → LowerFactorSpace n and derived the joint law as a relatively independent joining over the intrinsic factor. That derivation is what failed: it makes the latents conditionally independent of the structure given the intrinsic factor, so when that factor is trivial the latents are independent of the array. Austin's random complete bipartite graph X_{uv} = z_u ⊕ z_v (arXiv:0801.1698, §3.6) has trivial rank-2 factor and hidden colours that are correlated with the array while individually unrecoverable from it, so no such joining can represent it.

The primitive here is therefore the coupling P itself. The decoder direction is unchanged — structure recovered from latents — which was never the problem.

Local, and rank-truncated

Two further constraints, both load-bearing:

• Recovery is local. Global recovery of the whole lower factor from the whole latent cube would let a decoder read unrelated coordinates elsewhere in the universe, and would not descend to the eventual label-free kernels. Each block at A is recovered from localLatents A.
• Screening is rank-truncated. Higher-rank coordinates containing A legitimately share the latents at A, so screening a block from all higher ranks would be false. The rank-n block at A is screened from the other blocks of rank at most n.

Staging: U_A is not in scope at rank n

For A.card = n, the coordinate U_A is absent from RankLatentSpace S n outright, since RankLatentIndex S n ranges over supports of cardinality strictly below n (rankLatentIndex_ne_of_card_eq). So screening may put the entire RankLatentSpace S n on the far side without contradiction, and B ⊆ A within RankLatentIndex n automatically means B ⊊ A. Kallenberg's Lemma 7.24 is staged the same way — its coupled array is truncated below the working dimension, and the fresh uniforms enter only at the successor step, here supplied by the RankLatentSpace (n+1) ≃ᵐ RankLatentSpace n × (RankSupport S n → ℝ) split.

Acceptance tests

Two examples, each blind to the other's failure mode; a specification in this family needs both.

• Bipartite colours X_{uv} = z_u ⊕ z_v — correlation: hidden lower-rank latents may be correlated with the array while individually unrecoverable. This refutes factor-law coding, and passes here with screening non-vacuous, since the edge is a deterministic function of the two colours.
• I.i.d. edges X_{uv} = U_{uv} — staging: the top-rank latent is absent during screening and introduced only at randomization. The bipartite example cannot detect a rank off-by-one, because its edges use no rank-2 latent at all.

Local latents

@[reducible]

def RelSignature.LocalLatentIndex {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) (n : ℕ) : Type u_1

The latent coordinates visible at A: supports contained in A. Within RankLatentIndex n this automatically means proper subsets when A.card = n.

Equations

• RelSignature.LocalLatentIndex A n = RelSignature.LocalLatentIndexOver S.Vinfinite A n

instance RelSignature.instCountableLocalLatentIndexOfSrt {S : RelSignature} [Countable S.Srt] (A : Finset ((s : S.Srt) × S.Vinfinite s)) (n : ℕ) : Countable (LocalLatentIndex A n)

@[reducible, inline]

abbrev RelSignature.LocalLatentSpace {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) (n : ℕ) : Type u_1

The local latent space at A.

Equations

• RelSignature.LocalLatentSpace A n = (RelSignature.LocalLatentIndex A n → ℝ)

def RelSignature.localLatents {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) (n : ℕ) : S.RankLatentSpace n → LocalLatentSpace A n

Restriction of the latent array to the coordinates visible at A.

Equations

• RelSignature.localLatents A n = RelSignature.localLatentsOver A n

theorem RelSignature.measurable_localLatents {S : RelSignature} [Countable S.Srt] (A : Finset ((s : S.Srt) × S.Vinfinite s)) (n : ℕ) : Measurable (localLatents A n)

theorem RelSignature.rankLatentIndex_ne_of_card_eq {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) (B : S.RankLatentIndex n) : ↑B ≠ A

The staging lemma: at rank n the latent array carries no coordinate at a support of cardinality n. This is why screening may place the whole of RankLatentSpace S n opposite the rank-n block, and why B ⊆ A needs no separate properness side condition.

theorem RelSignature.rankLatentIndex_ssubset_of_card_eq {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} {n : ℕ} (hA : A.card = n) (B : LocalLatentIndex A n) : ↑↑B ⊂ A

Consequently a visible support at a rank-n set is a proper subset of it.

Blocks of raw relation coordinates

@[reducible]

def RelSignature.BlockIndex {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u_1

Raw relation coordinates whose tagged support is exactly A. Raw coordinates, not basis events: the eventual descent to label-free kernels is indexed by these.

Equations

• RelSignature.BlockIndex A = RelSignature.BlockIndexOver S.Vinfinite A

instance RelSignature.instCountableBlockIndexOfRel {S : RelSignature} [Countable S.Rel] (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Countable (BlockIndex A)

@[reducible, inline]

abbrev RelSignature.BlockSpace {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u_1

The rank-A block of the structure.

Equations

• RelSignature.BlockSpace A = (RelSignature.BlockIndex A → Bool)

def RelSignature.blockMap {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) : S.RelStructure S.Vinfinite → BlockSpace A

Read the block at A off a structure.

Equations

• RelSignature.blockMap A = RelSignature.blockMapOver A

theorem RelSignature.measurable_blockMap {S : RelSignature} [Countable S.Rel] (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Measurable (blockMap A)

The rank-truncated remainder

@[reducible]

def RelSignature.RestIndex {S : RelSignature} (n : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u_1

Coordinates of rank at most n other than those at A. The truncation is essential: coordinates of rank above n that contain A legitimately share A's latents, so screening against them would be false.

Equations

• RelSignature.RestIndex n A = RelSignature.RestIndexOver S.Vinfinite n A

instance RelSignature.instCountableRestIndexOfRel {S : RelSignature} [Countable S.Rel] (n : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Countable (RestIndex n A)

@[reducible, inline]

abbrev RelSignature.RestSpace {S : RelSignature} (n : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u_1

The remaining rank-≤ n structure.

Equations

• RelSignature.RestSpace n A = (RelSignature.RestIndex n A → Bool)

def RelSignature.restObservation {S : RelSignature} (n : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : S.RelStructure S.Vinfinite × S.RankLatentSpace n → RestSpace n A × S.RankLatentSpace n

The rank-truncated remainder observation: the other blocks of rank at most n, together with the whole latent array — which at rank n contains no coordinate at A.

Equations

• RelSignature.restObservation n A = RelSignature.restObservationOver n A

theorem RelSignature.measurable_restObservation {S : RelSignature} [Countable S.Rel] (n : ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Measurable (restObservation n A)

The specification

structure RelSignature.InfiniteRelExchangeableLaw.RankRepresentation {S : RelSignature} [Countable S.Srt] [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) (n : ℕ) : Type u

A joint rank-n representation. The primitive is the coupling P, not a coding map.

Deliberately independent of CoherentBasis: the specification mentions only the law, the raw relation coordinates, and the latent array. The refuted design was phrased against the basis and its factor maps, and that dependence is part of what led it to a factor-law primitive.

No existence theorem accompanies this definition, at any rank. Whether a non-trivial RankRepresentation n exists is the actual content of the converse, and is exactly what the refuted RankCoding design mistook for a bookkeeping step. Constructing one is expected to need a stationary extension to a fresh auxiliary vertex pool, transfer along that extension, and the polling clusters of Austin's Proposition 3.12.

• P : MeasureTheory.Measure (S.RelStructure S.Vinfinite × S.RankLatentSpace n)

  The coupling of the structure with the rank-n latents.

• isProbabilityMeasure_P : MeasureTheory.IsProbabilityMeasure self.P

  It is a probability measure.

• map_fst : MeasureTheory.Measure.map Prod.fst self.P = ↑M.law

  Its structure marginal is the law.

• map_snd : MeasureTheory.Measure.map Prod.snd self.P = S.rankLatentSource n

  Its latent marginal is the i.i.d. source.

• invariant (σ : ↥S.FinSuppPerm) : MeasureTheory.Measure.map (Prod.map (RelStructure.relabel ↑σ) ⇑(rankLatentRelabel σ n)) self.P = self.P

  Joint relabeling invariance: a relabeling acts on both coordinates at once.

• lower_recovers (A : Finset ((s : S.Srt) × S.Vinfinite s)) : A.card < n → ∃ (g : LocalLatentSpace A n → BlockSpace A), Measurable g ∧ blockMap A ∘ Prod.fst =ᵐ[self.P] g ∘ localLatents A n ∘ Prod.snd

  Local recovery: each block below rank n is a function of the latents visible at its own support — not of the latent array at large.

• screening (A : Finset ((s : S.Srt) × S.Vinfinite s)) : A.card = n → ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (localLatents A n ∘ Prod.snd) inferInstance) ⋯ (blockMap A ∘ Prod.fst) (restObservation n A) self.P

  Local screening-off, rank-truncated: the rank-n block at A is conditionally independent of the other rank-≤ n blocks and the latent array, given the latents visible at A. Kallenberg's X̃_A ⊥⊥_{ξ̂_A} (X ∖ X̃_A, ξ) at the working rank.