Documentation

Graphon.RelRankCoding

The inductive interface for the rank transition (R4 converse piece 3, #107) #

The two objects the rank recursion is organized around, and the base case.

A RankCoding n is a representation of the lower-rank factor by latents: a measurable map from the rank-n latent space to the rank-n factor space representing its law: it carries the latent source to the factor law and commutes with relabeling almost everywhere. A ShellProperty n is the conclusion the recursion needs at rank n: mutual conditional independence of the exact-anchor layers over the supports of rank n, together with per-support locality.

RankCoding is a factor-law coding, not an inductive hypothesis #

An earlier design proposed the recursion shell_of_rankCoding : RankCoding n → ShellProperty n followed by nextRankCoding : RankCoding n → ShellProperty n → Nonempty (RankCoding (n+1)). That first implication is false, and this header previously asserted it. The refutation is Austin's random complete bipartite graph (arXiv:0801.1698, §3.6, pp. 116–118): with X_{uv} = z_u ⊕ z_v for i.i.d. fair bits z_v, every singleton stabilizer algebra is trivial modulo the law, so lowerRankAlgebra 2 is trivial; but X₁₂ ⊕ X₁₃ ⊕ X₂₃ = 0 on every triangle, so the exact layers are not mutually independent. A RankCoding 2 nevertheless exists — the rank-2 factor law is a point mass, so a constant coding works — and hence RankCoding 2 ⇏ ShellProperty 2.

The example is pairwise independent, which is exactly why it separates the two-set theorem InfiniteRelExchangeableLaw.condIndep_fixingAlgebra — true, and maximal — from mutuality.

The failure is not repairable by coupling. relativeFactorCoupling makes latents conditionally independent of the structure given the intrinsic lower factor; here that factor is trivial, so it attaches unrelated uniforms. What a representation needs are the hidden colours z_v, which are correlated with the array without being recoverable from it. Austin's polling permutation correspondingly acts on an auxiliary quasifactor built from a fresh vertex pool, an object no relatively independent joining over lowerFactorMap contains.

So the objects here are honest but limited: RankCoding n records that the rank-n factor law is coded by latents, equivariantly and modulo null sets. It does not carry the joint information a recursion needs. A working induction must construct latents jointly with the array and impose a local screening-off relation, in the style of Kallenberg's Lemma 7.24, rather than derive one from factor-law coding.

Two halves, neither implying the other #

ShellProperty bundles both because neither follows from the other. Mutual independence given the whole lower-rank factor permits each individual conditional law to depend on all of it; it says nothing about that dependence being only through boundaryMap A. Conversely locality is a per-support statement and says nothing about joint behaviour across supports.

Contents #

The inductive datum #

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

A coding of the rank-n factor law by latents. This is not the inductive hypothesis of a working recursion — see the module header — but it is a true and reusable record of factor-law coding. "Representation" is about laws, not about images: map_f identifies the pushforward of the latent source with the factor law, and no pointwise surjectivity onto the factor space is asserted or used.

The equivariance clause is an almost-everywhere statement, and must be: lowerFactorSpaceEquiv σ n fixes the image of lowerFactorMap n, not the whole factor space, so the strict version is false already at n = 1.

Instances For

    The conclusion at rank n #

    source
    structure RelSignature.CoherentBasis.ShellProperty {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) [Countable S.Srt] [Countable S.Rel] (n : ℕ) :
    Prop

    The shell property at rank n: the two halves the recursion consumes.

    Both are stated against lowerRankAlgebra n and boundaryMap A — the objects the fixing-algebra machinery is phrased in — rather than against the represented factor. Transfer to comap (lowerFactorMap n) is a separate step, available from the eventwise generation of the lower-rank algebra together with the conditioning bridge.

    Instances For

      The base case #

      source
      noncomputable def RelSignature.CoherentBasis.RankCoding.rankOne {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) [Countable S.Srt] [Countable S.Rel] :
      B.RankCoding 1

      The rank-one coding. The coding map is the randomization adapter of #140 applied to the law of the rank-one factor, transported along rankLatentOneEquiv.

      The equivariance clause is not vacuous here. lowerFactorSpaceEquiv σ 1 permutes the empty-anchor basis indices, which name the same invariant event but are distinct coordinates of the Bool-cube; what is true is that it fixes the image of lowerFactorMap 1, so the clause holds almost everywhere and not identically. Rank one is therefore the first test that the field is correctly stated a.e.

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