The rank-one conditioning ladder (R4 converse piece 3, #107)

Under the rank-one coupling clauses, the singleton blocks — composed with the structure projection — are mutually conditionally independent given the full latent σ-algebra comap Prod.snd. This is the support-free core of the screening field; the per-support statement is a later specialization.

The ladder

The conditioning algebra climbs and then descends, each rung by a merged tool:

1. the singleton peel (#173) under the law, pulled to the coupling along Prod.fst (#175) — conditioning invariantAlgebra.comap fst;
2. down to comap (lowerFactorMap 1 ∘ fst) by the representable-conditioning transfer (#163), whose hypothesis is the eventwise generation of the rank-one factor (#157) pulled along fst;
3. up to the join with the latent algebra by the independent-refinement theorem (#174), whose hypothesis is the coupling's conditional-independence clause (#161/#177) joined freely with the conditioning (#176);
4. down to the latent algebra alone by #163 again, the representability of the join supplied by the resolution identity and eventuallyMeasurableSet_sup (#176).

Every conditioning move is modulo the coupling measure. No identification of the latent σ-algebra with the invariant algebra is asserted anywhere — the available statements are eventwise, and that is all the ladder uses.

def RelSignature.singletonBlockRead (S : RelSignature) (v : (s : S.Srt) × S.Vinfinite s) : S.RelStructure S.Vinfinite × S.RankLatentSpace 1 → BlockSpace {v}

The singleton block at v, read through the structure coordinate of the rank-one coupling space. Named so the family is fully typed at every use site; mentions no basis and no law, so it lives at the signature level.

Equations

• S.singletonBlockRead v = RelSignature.blockMap {v} ∘ Prod.fst

theorem RelSignature.measurable_singletonBlockRead {S : RelSignature} [Countable S.Rel] (v : (s : S.Srt) × S.Vinfinite s) : Measurable (S.singletonBlockRead v)

theorem RelSignature.comap_localLatents_one_snd {S : RelSignature} [Countable S.Srt] (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasurableSpace.comap (localLatents A 1 ∘ Prod.snd) inferInstance = MeasurableSpace.comap Prod.snd inferInstance

At rank one, local latents see everything: every latent coordinate has empty support, hence is visible at every A, so conditioning on the local latents is conditioning on the whole latent coordinate. A raw σ-algebra equality — no measure in sight.

theorem RelSignature.condIndepFun_blockMap_restObservation_one {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {P : MeasureTheory.Measure (S.RelStructure S.Vinfinite × S.RankLatentSpace 1)} [MeasureTheory.IsProbabilityMeasure P] (hladder : ProbabilityTheory.iCondIndepFun (MeasurableSpace.comap Prod.snd inferInstance) ⋯ S.singletonBlockRead P) {g₀ : LocalLatentSpace ∅ 1 → BlockSpace ∅} (hg₀ : Measurable g₀) (hrec : blockMap ∅ ∘ Prod.fst =ᵐ[P] g₀ ∘ localLatents ∅ 1 ∘ Prod.snd) (A : Finset ((s : S.Srt) × S.Vinfinite s)) (hA : A.card = 1) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (localLatents A 1 ∘ Prod.snd) inferInstance) ⋯ (blockMap A ∘ Prod.fst) (restObservation 1 A) P

Per-support screening at rank one. Given the ladder's conclusion — mutual conditional independence of the singleton blocks given the full latent σ-algebra — and the nullary recovery, the rank-one block at each support is conditionally independent of the rank-truncated remainder given the latents visible at that support. This is the screening field of a rank-one RankRepresentation, and it mentions no basis: everything it needs arrives through its hypotheses.

theorem RelSignature.CoherentBasis.iCondIndepFun_blockMap_singleton_comap_snd {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) [Fintype S.Srt] [Countable S.Rel] {P : MeasureTheory.Measure (S.RelStructure S.Vinfinite × S.RankLatentSpace 1)} [MeasureTheory.IsProbabilityMeasure P] (hfst : MeasureTheory.Measure.map Prod.fst P = ↑M.law) {g : S.RankLatentSpace 1 → B.LowerFactorSpace 1} (hg : Measurable g) (hres : B.lowerFactorMap 1 ∘ Prod.fst =ᵐ[P] g ∘ Prod.snd) (hci : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (B.lowerFactorMap 1 ∘ Prod.fst) inferInstance) ⋯ Prod.fst Prod.snd P) : ProbabilityTheory.iCondIndepFun (MeasurableSpace.comap Prod.snd inferInstance) ⋯ S.singletonBlockRead P

The conditioning ladder. Under a coupling of the law with the rank-one latents — structure marginal the law, rank-one factor resolved by a measurable latent read, structure and latent conditionally independent given the factor — the singleton blocks are mutually conditionally independent given the full latent σ-algebra.