R4 successor route A (Austin): polling → enriched object → kernel → noise outsourcing (#107)

[cameronfreer]

Child of #107 (R4 converse). Depends on the route-neutral gate #195 and the interface-only contracts #196.

One of two independent proofs of the successor theorem. Target:

nonempty_rankRepresentation_succ_via_austin :
  M.RankRepresentation n → Nonempty (M.RankRepresentation (n + 1))

Spine

polling → enriched lower-rank object → conditional kernel → noise outsourcing into uniform subset latents.

Austin explicitly distinguishes his abstract type-space / kernel ingredients from the classical functional representation, and explains that one passes from the former to the latter by noise outsourcing. His Proposition 3.12 supplies the polling-based conditional-independence engine, using finitely supported swaps into a spare vertex set.

Austin, On exchangeable random variables and the statistics of large graphs and hypergraphs, §§3.3 and 3.7: https://www2.math.ethz.ch/EMIS/journals/PS/images/getdoc4f78.pdf?article=124&id=546&mode=pdf

What this route pays for beyond the shared gate

• tail / polling conditional independence;
• the enriched lower-rank object;
• noise outsourcing, still required to reach this repository's uniform-real RankRepresentation interface.

That last item is not optional bookkeeping: the abstract kernel object is not yet a RankRepresentation, and the passage is where the uniform-real latents are produced.

Sequencing note

Given the infrastructure already built around fixing algebras, stationary extension, and pooled permutations, this is likely the better first implementation. It should be completed before the other hard core (#198) is started — the two spines are not to be blended.

Standing constraint

Austin §3.6's bipartite configuration is what refuted the shell theorem on 2026-08-03. It is a required regression here (#196), not an afterthought.

[cameronfreer]

Requirement recorded for this route, alongside the contract at #196.

Mixed-pool consumption must be witnessed by compiled code, not by issue text. RankSuccessor exposes no pooled carrier, so no final-output regression can observe whether a construction actually used boundary-crossing permutations. The property is formalized by the pooled gate's PooledRankExtension.map_restrict_embedding (merged in #201), which holds for every sortwise embedding.

This route's intermediate construction must therefore contain a compiled consumer of that theorem. A prose claim in an issue is not the evidence; the dependency has to appear in the proof term.