feat: pooled-latent gate stage 3 — joint restriction, law identity, and the four consequences (#195) - #201
Merged
Merged
Conversation
…tage 3) exists_perm_extend_of_injOn generalizes exists_perm_extend from an initial segment to an arbitrary finite domain, by the same Equiv.Set.compl argument. It is the finite-agreement step for the joint restriction theorem: on a joint cylinder, the combined vertex support is finite, and a pooled permutation must be found carrying the original embedding to an arbitrary one there.
stage 3) PooledRankExtension.map_restrict_embedding: for EVERY sortwise embedding e into the pooled carrier, restricting jointly — structure and latents along the same e — returns C.P exactly. Joint, so it recovers the (X, U_<n) law rather than only a structure window. Proof: joint-cylinder extensionality plus finite agreement with a mixed pooled permutation. On a cylinder the combined vertex support is finite; originalVertex v ↦ e v is a finite partial injection of the pooled carrier, extended by exists_perm_extend_of_injOn; full mixed invariance absorbs the permutation and permits choosing it per sort. latentIndexEmbed_eq_of_agree is the support-wise index lemma, proved with ABSTRACT carriers per the standing rule — instantiating at PoolVertex (a Sum) under Classical Finset.image otherwise clashes with the derived DecidableEq, which it did again here before the lemma was generalized. map_poolVertexEquiv is the reviewer's checkpoint: the canonical specialization, isolating map directions while the claim is still just an equality of joint laws, plus the agreement of any two extensions after that identification. Audit 384 -> 389.
…ap one (#195 stage 3) Bundles the canonical restriction at poolVertexEquiv.symm as the measurable equivalence pooledJointEquiv and cancels its pushforward, upgrading map_poolVertexEquiv_congr to the uncancelled equality PooledRankExtension.law_eq : Q.law = (C.pooledExtension).law so marginals, StationaryExtension, recovery and screening become transports of statements about C.P through one canonical identity rather than four bespoke measure arguments. Supporting carrier-generic machinery: latentIndexCongr (index bijection from a carrier equivalence, via latentIndexEmbed_comp and the identity embedding) and latentCongrOver (its measurable equivalence on the cube), both proved with abstract carriers. Audit 389 -> 391.
#195 stage 3, pin 1) localLatentsOver / blockMapOver / restObservationOver over an arbitrary carrier; the Vinfinite-indexed originals become compatibility aliases, so pooled recovery and screening instantiate this core rather than duplicating it. The module header records the boundary that matters: local and block observations read only coordinates supported inside a finite set and admit naturality along an arbitrary sortwise EMBEDDING, whereas the remainder is global — it ranges over every rank-≤n coordinate of the ambient carrier — so along an embedding into a larger carrier the target remainder sees coordinates the source cannot, and an embedding-level commuting law would be FALSE. It transports only along a carrier EQUIVALENCE, which for the pooled setting is poolVertexEquiv. Downstream cost of the aliasing was two simp sets that unfolded the old definitions directly (RelSingletonPeel, RelRankOneScreening); both now name the generic definition as well.
stage 3) measurePreserving_pooledJointEquiv packages the canonical identification as measure-preserving from Q.law to C.P — the handle that lets condIndepFun_comp_measurePreserving pull C.screening BACK to the pooled law, so conditional independence is never pushed forward and no further conditional-expectation theorem is needed. supportImage and latentIndexEmbed_subset_supportImage_iff are the bijection underlying local naturality: an embedding restricts to a bijection between supports inside A and those inside its image. Stated as an equivalence with pointwise lemmas first, per review, which also keeps the proof on Function.Injective.mem_finset_image rather than dependent sigma destructuring.
RelCoord.congrCarrier, the coordinate mirror of RelStructure.congrCarrier — the repository had RelCoord.map and support_map but no bundled equivalence. The remainder index is global, so its transport needs a genuine equivalence of coordinates rather than an embedding, and this is the reuse point for it. support_congrCarrier records that transport carries a support to its image.
…#195 stage 3) comap_measurableEquiv_comp: postcomposing an observation with a measurable EQUIVALENCE leaves the generated comap sigma-algebra unchanged. Named so the screening assembly can straighten a transported conditioning map without a further probabilistic lemma — measurability in both directions is exactly what makes the comap survive. restSpaceCongr bundles the remainder transport as a measurable equivalence (not merely an index bijection), built on RelCoord.congrCarrier and requiring a carrier EQUIVALENCE, since the remainder ranges over every rank-≤n coordinate of the ambient carrier.
…stage 3) Both follow the pinned pattern: index equivalence, space-level MeasurableEquiv via contravariant Equiv.arrowCongr, pointwise _apply, and an exact naturality theorem against the observation. localLatentIndexCongr needs no Finset.preimage — a support inside supportImage e A is the image of the part of A landing in it, so the inverse is a filter of A. blockIndexCongr keeps its inverse LOCAL to the exact-support subtype: exists_preimage_of_block draws the range witness for each argument from the coordinate's support being exactly supportImage e A, so nothing pretends the embedding is globally surjective. supportImage_injective generalized from equivalences to embeddings (only injectivity is used), and supportImage_support records that the image of a coordinate's support is the transported coordinate's support — the equation lemma for the noncomputable supportImage will not fire under rw. Audit 396 -> 400.
…sion (#195 stage 3) latentSourceOver_map_latentCongrOver is the generic exact source transport along a carrier equivalence — the same infinite-product coordinate-equivalence argument as source invariance. PooledRankExtension.map_snd: the pooled latent marginal is the pooled i.i.d. source, a transport of C.map_snd through the canonical identity. PooledRankExtension.toStationaryExtension: the structure marginal is a StationaryExtension M, both fields being the corresponding pooled field composed with Prod.fst. Support lemmas: pooledExtension_law_coe and rankLatentSource_eq_latentSourceOver bridge the alias boundary for rw, which cannot see through the coercion or the def.
The conditioning-algebra congruence lemma was duplicated verbatim as a private theorem in RelRankOneCoupling and RelRankOneScreening. Extracted once into ForMathlib/CondIndepSup as ProbabilityTheory.CondIndepFun.congr_cond, with both copies replaced by dot-notation calls; it handles the dependent comap_le proof by proof irrelevance after substituting the sigma-algebra equality. It is the lemma screening needs as its third step, alongside comap_measurableEquiv_comp — established shared glue with three consumers rather than speculative cleanup.
PooledRankExtension.lower_recovers: recovery holds on every pooled support below rank n, mixed supports included. C.lower_recovers is pulled back through measurePreserving_pooledJointEquiv's quasiMeasurePreserving ae_eq_comp, and the decoder is conjugated through the local and block measurable equivalences — the only a.e. step is the transported identity itself, with no manual null-set rewriting. The pooled support is presented once as the image of an original one (supportImage_symm_supportImage, card_supportImage) via an obtain with rfl, which avoids dependent ▸ transports entirely.
…195) restObservationOver_congrCarrier is the missing naturality: observing after transporting the joint object back from W to V equals observing on W and reindexing both remainder outputs. Pointwise rfl after funext, as expected, and equivalence-only throughout. PooledRankExtension.screening is then pure assembly in the three named steps: condIndepFun_comp_measurePreserving on measurePreserving_pooledJointEquiv, CondIndepFun.comp with the inverse output equivalences (post-composition never touches the dependent proof, which is why the coercion cannot be rewritten inside the conditioning algebra), and CondIndepFun.congr_cond with comap_measurableEquiv_comp. No conditional-expectation or dependent-proof manipulation appears. All four route-neutral consequences of the gate are now proved. Audit 405 -> 407.
…header, drop superseded restatements (#195) CondIndepSup now says three closure properties and documents CondIndepFun.congr_cond, in the module header and the Graphon.lean bullet. RelPooledAcceptance's module header names law_eq and all four consequences, so it stays authoritative when the umbrella inventory is trimmed (#167). Removed two superseded restatements with no consumers: map_poolVertexEquiv_congr (strictly weaker than law_eq) and pooledExtension_map_restrict_embedding (identical to (C.pooledExtension).map_restrict_embedding with no simpler hypotheses). Neither was audited, so the audit count is unchanged.
This was referenced Aug 16, 2026
Open
Open
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stage 3 of the pooled-latent extension gate (#195; #107 remains open) — the organizing theorem, the canonical law identity, the carrier-parametric observation layer, and all four route-neutral consequences. Nothing route-specific enters: no fresh rank-
nlatent extraction and nothing at rankn + 1.The organizing theorem
PooledRankExtension.map_restrict_embedding: for every sortwise embeddinge : ∀ s, Vinfinite S s ↪ PoolVertex S s,Being joint is the point — structure and latents restricted along the same embedding — so it recovers the
(X, U_{<n})law and says strictly more than a structure-only window theorem. Proved by joint-cylinder extensionality plus finite agreement with a mixed pooled permutation: on a cylinder the combined vertex support is finite,originalVertex v ↦ e vthere is a finite partial injection of the pooled carrier, andexists_perm_extend_of_injOn(a generalization of the repository's initial-segment lemma to arbitrary finite domains) extends it. The full mixed action is what permits choosing the permutation independently on each sort, with no finite-support or uniform-bound issue.The canonical law identity
Bundling the canonical restriction as the measurable equivalence
pooledJointEquivand cancelling its pushforward gives— a uniqueness theorem: every pooled rank extension is the cheap one. Every consequence below is therefore a transport through one identity rather than a separate measure argument.
measurePreserving_pooledJointEquivpackages it as measure-preserving fromQ.lawtoC.P, which is what lets conditional independence be pulled back rather than pushed forward.The observation layer (
Graphon/RelObservationGeometry.lean, new)localLatentsOver,blockMapOver,restObservationOverover an arbitrary carrier, with theVinfinite-indexed originals as compatibility aliases. The three do not transport equally, and the difference is truth rather than proof effort: the first two are local and admit naturality along an arbitrary embedding; the remainder is global — it ranges over every rank-≤ ncoordinate of the ambient carrier — so along an embedding into a larger carrier the target remainder sees coordinates the source cannot, and an embedding-level commuting law would be false. It transports only along a carrier equivalence, and the type signatures enforce that.Each observation gets the same four-part API: index equivalence, space-level
MeasurableEquivvia contravariantEquiv.arrowCongr, pointwise_apply, and an exact naturality theorem. The block inverse is kept local to the exact-support subtype, where every argument provably lies in the embedding's range; nothing pretends the embedding is globally surjective.The four consequences
map_snd— the pooled latent marginal is the pooled i.i.d. source, via the new generic source transport along a carrier equivalence.toStationaryExtension— the structure marginal is aStationaryExtension M.lower_recovers— local recovery on every pooled support below rankn, withC.lower_recoverspulled back throughae_eq_compand the decoder conjugated through the local and block equivalences. The only almost-everywhere step is the transported identity itself.screening— screening on every pooled support of rankn, as pure assembly in three named steps:condIndepFun_comp_measurePreserving,CondIndepFun.compfor the block and remainder codomains, andCondIndepFun.congr_condwithcomap_measurableEquiv_compfor the conditioning algebra. No conditional-expectation or dependent-proof manipulation appears.Shared glue extracted
ProbabilityTheory.CondIndepFun.congr_condwas duplicated verbatim as a private theorem inRelRankOneCouplingandRelRankOneScreening; it now lives once inForMathlib/CondIndepSup.leanwith both copies replaced and this PR as its third consumer.comap_measurableEquiv_compis the companion: postcomposing an observation with a measurable equivalence leaves the generated σ-algebra unchanged — a measurable equivalence changes coordinates, not information.Bookkeeping
RelObservationGeometry,RelPooledAcceptance(plus stage-1/2 modules already merged).scripts/axiom_audit.leanand the intended-set literal inscripts/check_census_and_axioms.py.lake buildclean (3403 jobs), census + axiom audit pass, zero sorries.With this the route-neutral gate is complete, and the next decision is the route fork at #196.