Rank-one local recovery (R4 converse piece 3, #107)

The lower_recovers field of a rank-one RankRepresentation: the block strictly below rank one — the nullary block, at support ∅ — is almost everywhere a measurable function of the latents visible at ∅.

The argument is coordinatewise and countable. Each nullary relation coordinate is an event of fixingAlgebra ∅ = invariantAlgebra; the eventwise generation of the rank-one factor (exists_comap_lowerFactorMap_one_ae_eq, #157) supplies, per coordinate, a factor event agreeing with it modulo the law; a decide-indicator coding turns the chosen factor events into a measurable map LowerFactorSpace 1 → BlockSpace ∅; and the resolution identity of the coupling replaces the factor read of the structure by the latent read. Countably many null coordinate disagreements combine by ae_all_iff, and the latent read factors exactly through localLatents ∅ 1, which at rank one is a bijective reindexing.

Stated over an abstract coupling with the two clauses it consumes — the structure marginal and the resolution identity — rather than over rankOneLatentCoupling itself, so the final assembly passes the clauses it destructured. Everything is modulo the coupling measure: no claim is made that the nullary block is a strict function of the latent, and none is available.

theorem RelSignature.CoherentBasis.exists_blockMap_recovery_of_card_lt_one {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) [Countable S.Srt] [Countable S.Rel] {P : MeasureTheory.Measure (S.RelStructure S.Vinfinite × S.RankLatentSpace 1)} (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) (A : Finset ((s : S.Srt) × S.Vinfinite s)) (hA : A.card < 1) : ∃ (g₀ : LocalLatentSpace A 1 → BlockSpace A), Measurable g₀ ∧ blockMap A ∘ Prod.fst =ᵐ[P] g₀ ∘ localLatents A 1 ∘ Prod.snd

Rank-one local recovery. Under any coupling of the law with the rank-one latents whose structure marginal is the law and which resolves the rank-one factor through a measurable latent read, every block of rank strictly below one — the nullary block — is almost everywhere a measurable function of the latents visible at its own support.