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

Graphon.lean

@@ -48,6 +48,7 @@ import Graphon.RelObservationGeometry
 import Graphon.RelPooledLatents
 import Graphon.RelPooledExtension
 import Graphon.RelPooledAcceptance
+import Graphon.RelAustinPolling
 import Graphon.RelRankSuccessorContract
 import Graphon.DigraphCoordSupport
 import Graphon.RelBipartiteRegression
@@ -273,6 +274,7 @@ in Lean 4 using Mathlib.
 * `Graphon.RelPooledAcceptance` — R4 converse (#107), stage 3 of the pooled-latent extension gate, organizing result: **the joint restriction theorem**. For *every* sortwise embedding `e : ∀ s, Vinfinite S s ↪ PoolVertex S s`, restricting a pooled rank extension jointly — structure and latents along the same embedding — returns the representation exactly: `Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P`. Being **joint** is the point: 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, the assignment `originalVertex v ↦ e v` there is a finite partial injection of the pooled carrier, and `exists_perm_extend_of_injOn` extends it; the full mixed invariance then absorbs the permutation, which is also what lets it be chosen independently on each sort with no finite-support or uniform-bound issue. The four route-neutral consequences follow from it: `map_snd` (the pooled latent marginal is the pooled i.i.d. source), `toStationaryExtension` (the structure marginal is a `StationaryExtension M`), `lower_recovers` (local recovery on every pooled support below rank `n`, the decoder conjugated through the local and block measurable equivalences), and `screening` (screening on every pooled support of rank `n`, a pullback through `measurePreserving_pooledJointEquiv` followed by `CondIndepFun.comp` on the codomains and `CondIndepFun.congr_cond` with `comap_measurableEquiv_comp` on the conditioning algebra — no conditional-expectation reasoning). `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization; bundling that restriction as the measurable equivalence `pooledJointEquiv` and cancelling it yields **`PooledRankExtension.law_eq`, a uniqueness theorem** — every pooled rank extension *is* the cheap one. Marginals, the `StationaryExtension` structure, recovery and screening therefore transport from `C.P` through one canonical law identity rather than requiring separate measure arguments
 * `Graphon.RelRankSuccessorContract` — R4 converse (#107), **interface only**: the shared witness both successor constructions must produce, and the two identically typed statements they target. `RankSuccessor C` carries the next representation together with **exact truncation compatibility**, `next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P` — the observable that makes the statement mention `C` at all. A theorem returning merely `Nonempty (RankRepresentation (n + 1))` could ignore `C` and produce an unrelated representation, which is the same underdetermination that sank the earlier shell attempt. The witness carries **no independence field** beyond `RankRepresentation`'s own, and **no equality between the two routes' outputs** is asserted — they prove one statement by different means and will not produce canonically equal representations. `AustinSuccessor` and `KallenbergSuccessor` are the same proposition by construction, so whichever lands first discharges the induction while the other remains an independent proof. Regression: `truncation_zero` shows the truncation equation is **automatic at rank zero** — the rank-zero latent cube is a single point, so both sides are determined by their structure marginals, which the representation axioms already pin, and the base case imposes nothing extra. The witness exposes no pooled carrier, so whether a construction genuinely used boundary-crossing permutations is observed by the pooled gate's `map_restrict_embedding` rather than by any final-output check here; each route's intermediate construction consumes that theorem. Adversarial examples are kept in route-independent regression modules, outside this interface
 * `Graphon.DigraphCoordSupport` — shared regression infrastructure: the support of a digraph coordinate is the pair of its endpoints, with the off-diagonal cardinality corollary, over an arbitrary vertex type. A bridge module so that the D1 carrier `Graphon.InfiniteDigraph` does not acquire a dependency on the equality-pattern layer where `RelCoord.support` lives — the same separation `Graphon.SimpleGraphDigraphBridge` maintains for `SimpleGraph`. Stated with `[DecidableEq V]` and proved by membership, because `RelCoord.support` is built classically and over a concrete carrier the natural instance is not definitionally the classical one, so an image-shaped statement would not apply at the sites that need it
+* `Graphon.RelAustinPolling` — R4 converse (#107/#197), **route A (Austin) unit 1**: pooled polling. Austin's Proposition 3.12 polls with swaps into a *spare vertex set*, and the pooled carrier is exactly that — `PoolVertex` is `Vinfinite ⊕ Vinfinite` with `originalVertex = Sum.inl` and `poolVertex = Sum.inr`, so the halves are disjoint definitionally, and the extension's invariance under the **full** pooled permutation family means the swaps carry no finite-support side condition. **The geometry is the delicate part**: the observed blocks are confined to the original half and the poll to supports containing a spare vertex, so the two families are disjoint by construction — reading the blocks through the canonical `pooledJointEquiv` instead is tempting, since it makes the transport to `C.P` exact, but it is wrong, because that bijection sends blocks across *both* summands and they would then overlap the poll. **The seam is an enriched law, not `C.P`**: Austin's polling data is the family of *mixed* clusters — those not wholly original, all-spare included — spanning the two halves, and forgetting it into a bare `C.P` statement would discard what the successor construction consumes, so `enrichedPollingLaw` retains the whole pooled rank-`n` latent array and the clusters alongside the original structure and old latents, with `enrichedPollingLaw_map_fst` recovering `C.P` exactly through `map_restrict_embedding` at the original-vertex embedding. `pollingCond` pins the conditioning concretely — the whole pooled rank-`n` latent array plus the mixed clusters — since an existential factor could be the whole joint object and make the conclusion vacuous. `PooledPollingWitness.mutualCondIndep` is `iCondIndepFun` over the **entire** rank-`n` block family: mutual, not pairwise, which is Austin's actual conclusion and what the #196 battery keeps honest. Needs only the ambient `Countable` assumptions — because the conditional independence comes from the assumed screening contract rather than from a polling argument, the `Fintype S.Srt` hypothesis the fixing-algebra stack carries is not required; rank zero is routed to `nonempty_rankRepresentation_one` with `truncation_zero`, respecting `stepKernel`'s deliberate lack of an `A = ∅` realization theorem
 * `Graphon.RelBipartiteRegression` — R4 converse (#107/#196): the **bipartite regression** for the successor contract, a hand-built rank `1 → 2` witness over `digraphSig` whose purpose is to test that `RankSuccessor` is an expressive specification *before* either route is attempted. Each vertex carries an i.i.d. colour on its own fresh singleton coordinate and the edge is the parity, so the diagonal is constantly `false` for free. Three independent things make it a regression rather than a construction: the array law is defined **from the fresh singleton layer alone** and the rank-one coupling as the independent product `bipartiteLaw × rankLatentSource 1`, so `rankTwoCoupling_truncation` compares two separately described couplings and genuinely consumes the source factorization; the rank-two block decoder recovers **both** directed coordinates `X_uv` and `X_vu` as the same parity, exhibiting symmetry as a property of this law rather than of the signature; and `not_indepFun_rankTwoCoupling` is **numerical** — the edge and colour-parity events coincide with probability `1/2` against a product of marginals `1/4`, which a constant edge could not achieve even though it too would be "a function of the colours". `bipartiteSuccessor : RankSuccessor rankOneRep` is the witness itself
 * `Graphon.RelIidEdgeRegression` — R4 converse (#107/#196): the **i.i.d.-edge regression** for the successor contract, a hand-built rank `2 → 3` witness over `digraphSig` that tests **staging and recovery** where the bipartite regression tested independence and symmetry. The array is keyed by a coordinate's *support*, which gives symmetry (`X_uv = X_vu`) and the empty diagonal by construction — each is still proved from a support computation, but neither requires a choice of orientation. Two things make it a regression rather than a construction. First, recovery is genuinely staged: at rank three a two-point block is decoded from the latent coordinate at its own support — carried by the rank-three array because `2 < 3` — while at rank two the same blocks are not latent-measurable at all, so the two ranks exercise opposite sides of `lower_recovers`. Second, rank-two screening is a genuine conditional-independence statement: the block reads one coordinate of the edge source and the remainder reads the others plus the whole latent array, so screening follows from **independence**, not from determinism as in the bipartite case. `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly `1/2`, which rules out a *constant* block; that the block is not measurable from the old latents is a separate fact, supplied by the product independence built into the rank-two coupling. The private conditional-independence lemma is stated for abstract σ-algebras rather than for the two coordinates of a product because the ambient measure is a pushforward of a product and the current API only transports conditional independence **backward**: a source-level proof would require a new forward law-transport theorem, whereas transporting the unconditional independence needs no new theorem. `iidEdgeSuccessor : RankSuccessor rankTwoRep` is the witness itself
 * `Graphon.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `RelCoord`s and finitely many latent indices — whose combined vertex support is one finite `Finset (Σ s, Vinfinite S s)` and so touches only finitely many sorts; the injection is matched there by extending it on each active sort, taking the identity elsewhere, and maximizing finitely many support bounds. The coarser `restrictFin` cylinder family would instead force a uniform all-sort bound that no self-injection need admit