R4 successor route B (Kallenberg): direct correlated subset latents — independent check (#107)

[cameronfreer]

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

The second, independent proof of the successor theorem. Target:

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

Spine

Directly construct the correlated subset latents, with recovery and screening — attacking the central correlated-latent construction head-on rather than through polling and an enriched lower-rank object.

What this route pays for beyond the shared gate

The coherent simultaneous randomization and selection of subset latents. This is a genuine hard core, not a repackaging of the other route's final step.

Why build it after a route already lands

The value is independent auditing: this route attacks the correlated-latent construction from a different direction, so a defect in either spine is unlikely to be shared. The outputs will not be canonically equal representations, and no equality between them should be stated (#196).

Sequencing

Start only once the first route (#197) is complete. The two spines are not to be blended; pricing for this one is re-done after the first lands, since the shared gate's actual cost will then be known.

[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.