R4: pooled polling witness from rank screening and weak union (#197 unit 1)

[cameronfreer]

Unit 1 of the Austin route (#197; #107 remains open): the pooled polling witness, obtained from the assumed rank-n screening contract together with weak union.

This does not formalize Austin's Proposition 3.12. The construction follows Austin — a spare vertex reservoir, mixed clusters straddling it, and an enriched law that carries the polling data forward — but the conditional-independence engine is not his. RankRepresentation.screening is a field, an inductive hypothesis assumed at rank n, and its remainder already contains every other rank-≤ n block together with the whole pooled latent array. Weak union converts that directly into the mutual statement, so the tail-polling argument is not needed at this inductive stage and no tail machinery appears. The module says exactly this, and the now-unused polling-infrastructure import is dropped rather than a dependency manufactured.

The geometry

PoolVertex S s is Vinfinite S s ⊕ Vinfinite S s, with originalVertex = Sum.inl and poolVertex = Sum.inr, so the halves are disjoint definitionally and a PooledRankExtension is invariant under the full pooled permutation family.

The observed blocks are confined to the original half; the poll is confined to supports carrying at least one spare vertex. The two families are therefore disjoint by construction, which is the point — a block that could itself lie in the poll would make the conditional independence say nothing. Reading the blocks through the canonical pooledJointEquiv instead is tempting, because it makes the transport to C.P an exact identification, but it is wrong: that bijection sends blocks across both summands, and they would overlap the poll.

MixedClusterIndex means not wholly original — all-spare supports included, their original part being empty and hence proper. It is the negation of "wholly original", not a demand that both halves be met.

The seam is an enriched law

Forgetting the polling data into a bare C.P statement would discard what the successor construction consumes. enrichedPollingLaw retains the mixed clusters and the whole pooled latent array alongside the original structure and old latents, and enrichedPollingLaw_map_fst recovers C.P exactly, through Q.map_restrict_embedding at the original-vertex embedding — so the pooled gate theorem of #195 is a compiled dependency, verified by a transitive dependency walk with a control theorem that does not reach it.

The pooled latent array is carried because Q.screening's remainder contains it in full and weak union conditions on exactly that lower-rank factor. Every pooled index has cardinality < n, so the conditioning reveals no rank-n block.

The argument

• condIndep_weak_union — if X ⊥ (Y, Z) | W and W ≤ Z then X ⊥ Y | Z. Neither Mathlib nor this repository had it. W ≤ Z is a hypothesis rather than a conclusion shape, so the result conditions on exactly Z, which is what keeps one fixed conditioning algebra across every stage of the peel.
• restToPollingData — the screening remainder computes both the accumulated blocks and the entire polling conditioning, as a measurable factorization with an exact identity, so CondIndepFun.comp consumes Q.screening directly. This records what the remainder supplies rather than proving measurability coordinate-by-coordinate and discarding the assembled map.
• polling_condExp_insert — the peel step as a direct conditional-expectation identity, so it drops into Finset.induction_on (with Finset.set_biInter_insert and Finset.prod_insert) and no dependent tuple reindexing happens inside the induction.
• iCondIndepFun_originalBlock_sourcePollingCond — mutual conditional independence of the entire rank-n block family under Q.law. Mutual, not pairwise and not one-block-against-the-rest; the R4: successor contracts (interface-only) + shared regressions for both routes (#107) #196 battery exists to keep that distinction honest. Named at top level so it is independently reviewable.
• pooledPollingWitness — pure transport. The block codomains genuinely differ, and blockSpaceCongr with enrichedBlock_comp_enrichedPollingMap relates them exactly, so no coercion is improvised inside the constructor.

Scope

Only the ambient Countable assumptions are needed. Because the conditional independence comes from the assumed screening contract rather than from a polling argument, the Fintype S.Srt hypothesis that the fixing-algebra stack carries is not required — it was inherited from the originally planned route and dropped once weak union replaced the tail engine. Rank zero is routed to nonempty_rankRepresentation_one with truncation_zero, respecting stepKernel's deliberate lack of an A = ∅ realization theorem. Nothing here asserts that the two routes' outputs agree, and no Kallenberg machinery appears.

mem_supportImage_iff is added to RelObservationGeometry: a third site where a classical DecidableEq used to form an image is not definitionally the natural instance available over a concrete carrier — here PoolVertex, whose Sum supplies one — so the membership form, carrying no instance in its type, is stated once alongside the geometry.

Bookkeeping

Audit 426 → 433 in both scripts/axiom_audit.lean and the intended-set literal in scripts/check_census_and_axioms.py. Gates: lake build clean (3409 jobs), census + axiom audit pass, zero sorries, no warnings.