R4 gate 1a: route-neutral pooled-latent extension gate (#107)

Child of #107 (R4 converse). The route-neutral pooled-latent extension gate: the last pooled-latent gate before the successor layer.

Why it exists

RelExtensionLift (#183) is split-equivariant and only split-equivariant: a boundary-crossing permutation has no action on RankLatentSpace S n, which indexes latents by original-carrier supports. Polling needs a latent object carrying a genuine mixed pooled action. That object is this gate.

Pinned contract

A three-field structure over a rank-n representation, with no independence field:

structure PooledRankExtension (C : M.RankRepresentation n) where
  law :
    ProbabilityMeasure
      (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)
  map_restrictOriginal :
    law.map (Prod.map (restrictOriginal S) (restrictOriginalLatents S n)) = C.P
  invariant :
    ∀ ρ : ∀ s, Equiv.Perm (PoolVertex S s),
      law.map (Prod.map (RelStructure.relabel ρ) (pooledRankLatentRelabel ρ n)) = law

The action is the full sortwise pooled permutation family, not a finitely supported substitute. Finite support is an artifact of the coherent-basis / fixing-algebra layer, not of latent cubes: any sortwise permutation reindexes finite supports and preserves cardinality, hence induces a measurable equivalence preserving the i.i.d. source. Whatever polling ultimately uses should be a corollary of the full action; StationaryExtension already quantifies over all mixed permutations, and the primitive here should not be weaker.

Acceptance test

Joint, not the structure marginal. A finite mixed window — preferably the stronger restriction along any sortwise embedding of an infinite copy — must recover the corresponding joint (X, U_{<n}) law. A structure-only window theorem would add nothing beyond StationaryExtension.law_map_restrict_window.

Derived in this unit

the pooled latent marginal is the pooled i.i.d. source;
the structure marginal is a StationaryExtension M;
exact joint mixed-window / infinite-copy marginals;
local recovery for pooled supports of cardinality < n;
screening for pooled supports of cardinality = n.

The last two are the existing rank-n properties transported to mixed pooled supports. They are route-neutral and belong before the fork.

Explicitly out of scope

Fresh rank-n latent extraction; recovery at rank n + 1; screening at rank n + 1. Those are the successor constructions and live in the fork issues. This gate must contain no route-specific field and name no route — that neutrality is what keeps both proofs available.

Implementation order

pooled latent geometry and the mixed action;
the three-field structure and the cheap constructor (transport along poolVertexEquiv);
current-rank recovery and screening consumers.

Prerequisite

The joint self-injection invariance theorem (PR #194) — the cheap constructor depends on it.

Decision: no `Fintype` on sorts

Settled, not open:

the pooled latent indices, spaces, action, and this contract do not carry [Fintype S.Srt]; at worst such a hypothesis would belong only on an existence theorem;
feat: joint invariance under sortwise self-injections — pooled-latent gate risk (#107) #194's headline theorem is generalized using finite coordinate cylinders — finitely many RelCoords and finitely many RankLatentIndexes, whose combined vertex support is one finite Finset (Σ s, Vinfinite S s) and hence touches finitely many sorts;
[Fintype S.Srt] was an artifact of the coarse restrictFin cylinder family used in the first proof, not a genuine obstruction.

Prerequisite cleared: PR #194 is merged (c4051f4). RankRepresentation.map_prodMap_restrict_self holds under RankRepresentation's own hypotheses — no [Fintype S.Srt] — so the pooled latent indices, spaces, action, and this contract inherit no finiteness hypothesis on sorts, as decided above.

Implementation may now begin at stage 1 (pooled latent geometry and the mixed action). #195 remains open.

Merge pull request #199 from cameronfreer/r4-pooled-latents

Stage 1 merged (#199, 9b911c1). Stage 2 is under way on r4-pooled-extension.

Bridge requirement recorded and satisfied. The two extensional bridges are proved and pushed:

rankLatentRelabel_eq_latentRelabelOver — the rank-indexed action is the carrier-parametric action at Vinfinite S;
rankLatentReindex_eq_latentRestrictOver — the self-injection reindexing of feat: joint invariance under sortwise self-injections — pooled-latent gate risk (#107) #194 is restriction along that injection in the core.

Both are genuine equalities rather than rfl: the two constructions choose different Decidable instances under open scoped Classical, which is invisible propositionally. Also added latentRestrictOver_comp, the functoriality the constructor needs.

The constructor's derivation, for the record. Writing pv for poolVertexEquiv and ov for originalVertex, the transport is comap pv on structures and restriction along pv on latents. Then:

restrictOriginal ∘ transport = comap (pv ∘ ov), and pv ∘ ov is a self-injection of the original carrier — so map_restrictOriginal is exactly feat: joint invariance under sortwise self-injections — pooled-latent gate risk (#107) #194 applied to that injection;
relabel ρ ∘ transport = transport ∘ relabel κ where κ = pv ∘ ρ ∘ pv⁻¹ is a permutation of the original carrier — so invariant for the full mixed family is feat: joint invariance under sortwise self-injections — pooled-latent gate risk (#107) #194 applied to κ, a permutation being in particular an injection.

This is what "once the self-injection theorem exists, full mixed pooled invariance costs no additional mathematics" comes to concretely: both fields of the three-field structure reduce to #194, with the bridges carrying the rank-indexed statements into the generic API. #195 remains open.

feat: the pooled rank extension and its cheap constructor (#195 stage 2)

Merge pull request #200 from cameronfreer/r4-pooled-extension

Stage 2 merged (#200, f714a36). PooledRankExtension and RankRepresentation.pooledExtension are on master; audit 384.

Stages 1 and 2 of the implementation order are therefore complete. Remaining in this gate, per the pinned contract:

the joint acceptance theorem — a finite mixed window, or preferably the stronger restriction along any sortwise embedding of an infinite copy, recovering the corresponding joint (X, U_{<n}) law;
the pooled latent marginal is the pooled i.i.d. source;
the structure marginal is a StationaryExtension M;
local recovery for pooled supports of cardinality < n;
screening for pooled supports of cardinality = n.

The last two are the existing rank-n properties transported to mixed pooled supports, and are route-neutral. Fresh rank-n latent extraction and anything at rank n + 1 stay outside, as does anything route-specific. #195 remains open.

feat: the joint restriction theorem and transport characterization (#195

feat: canonical law identity — every pooled rank extension is the che…

feat: carrier-parametric observation layer with the transport boundary (

feat: measure-preserving canonical equivalence + support transport (#195

feat: bundled coordinate carrier equivalence (#195 stage 3)

feat: conditioning-algebra invariance + bundled remainder equivalence (…

feat: local and block observation bundles with exact naturality (#195 …

feat: consequences 1 and 2 — pooled latent marginal, stationary exten…

refactor: extract CondIndepFun.congr_cond as shared glue (#195 stage 3)

feat: consequence 3 — local recovery on pooled supports (#195 stage 3)

feat: consequence 4 — screening on pooled supports; stage 3 complete (#…

docs: cleanup before merge — three closure properties, authoritative …

Merge pull request #201 from cameronfreer/r4-pooled-acceptance

Stage 3 merged (#201, b14fea0). The route-neutral pooled-latent extension gate is complete, with all three stages on master and the audit at 407.

What the gate now provides:

PooledRankExtension — the three-field structure, full mixed action, no independence field;
RankRepresentation.pooledExtension — the cheap constructor, both laws reducing to the self-injection invariance theorem (feat: joint invariance under sortwise self-injections — pooled-latent gate risk (#107) #194);
PooledRankExtension.map_restrict_embedding — the joint restriction theorem for every sortwise embedding into the pooled carrier, mixed windows included;
PooledRankExtension.law_eq — the uniqueness identity: every pooled rank extension is the cheap one;
the four route-neutral consequences: map_snd, toStationaryExtension, lower_recovers (pooled supports of size < n), screening (pooled supports of size n).

Everything excluded by the contract stayed excluded: no fresh rank-n latent extraction, nothing at rank n + 1, and no route named anywhere in the gate.

The next decision is the fork itself — #196 (interface-only successor contracts and the shared bipartite / i.i.d. / rank-zero / mixed-pool regressions), then #197 (Austin) with #198 (Kallenberg) as the independent check. #195 remains open pending closure by the maintainer.

Merge pull request #204 from cameronfreer/r4-pooled-acceptance-lint

Closing: the route-neutral pooled-latent extension gate is complete on master, and the one review cleanup is merged (#204, 901e524).

What landed

Unit	PR	Merge
Joint self-injection invariance (prerequisite)	#194	`c4051f4`
Stage 1 — pooled latent geometry, full mixed action	#199	`9b911c1`
Stage 2 — three-field structure, cheap constructor	#200	`f714a36`
Stage 3 — joint restriction, law identity, four consequences	#201	`b14fea0`

Contract as pinned, and as delivered

PooledRankExtension — exactly three fields: joint law, exact restriction to C.P, invariance under the full pooled family. No independence clause.
RankRepresentation.pooledExtension — the cheap constructor; both laws reduce to map_prodMap_restrict_self, via a self-injection and via the conjugate permutation.
PooledRankExtension.map_restrict_embedding — the joint acceptance theorem, for every sortwise embedding, mixed windows included.
PooledRankExtension.law_eq — the canonical uniqueness identity, which makes each consequence a transport rather than a separate measure argument.
The four route-neutral consequences: pooled latent marginal, StationaryExtension, local recovery below rank n, screening at rank n.

Exclusions held: no fresh rank-n latent extraction, nothing at rank n + 1, no route named anywhere in the gate, no Fintype hypothesis on sorts, zero sorries, standard axioms only.

Mixed-pool consumption is observed here rather than at the successor interface; each route owes a compiled consumer of map_restrict_embedding (recorded on #197 and #198).

Next: #196 (successor contract and shared regressions) is the remaining shared unit, then the route fork. #107 remains open.

Navigation Menu

Repository navigation

R4 gate 1a: route-neutral pooled-latent extension gate (#107) #195

Why it exists

Pinned contract

Acceptance test

Derived in this unit

Explicitly out of scope

Implementation order

Prerequisite

Decision: no `Fintype` on sorts

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

R4 gate 1a: route-neutral pooled-latent extension gate (#107) #195

Description

Why it exists

Pinned contract

Acceptance test

Derived in this unit

Explicitly out of scope

Implementation order

Prerequisite

Decision: no Fintype on sorts

Activity

cameronfreer commented on Aug 15, 2026

cameronfreer commented on Aug 15, 2026

cameronfreer commented on Aug 15, 2026

cameronfreer commented on Aug 16, 2026

cameronfreer commented on Aug 18, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

Decision: no `Fintype` on sorts