R4: successor contracts (interface-only) + shared regressions for both routes (#107)

[cameronfreer]

Child of #107 (R4 converse). Depends on the route-neutral gate #195.

Compile both successor constructions as interface-only structures and theorem statements, before either hard core is attempted, and run the shared regression suite against both.

The two theorems are identically typed

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

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

Same type, two proofs. They will not produce canonically equal representations, and no equality between their outputs should be stated or assumed; the point is two independent proofs of one existence theorem, not a canonical construction.

The public induction theorem uses whichever route lands first. The other remains an independently audited proof path — which is the entire value of building the second.

Regressions, run against both

• bipartite (the Austin §3.6 configuration that refuted the shell theorem on 2026-08-03);
• i.i.d.;
• rank-zero / nullary;
• mixed-pool.

Running these against interface-only statements is what makes the later pricing honest: a regression that cannot even be stated against one route's interface is a design defect found cheaply.

Deliverable

Statements and structures only, with no proof of either successor theorem. The hard cores are #197 and #198.

[cameronfreer]

Contract landed on r4-successor-contract (interface only, no construction).

RankSuccessor C carries the next representation together with the load-bearing observable:

truncation : next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P

Exact, law-level, not a.e. and not up to isomorphism. Without it a theorem returning merely Nonempty (RankRepresentation (n + 1)) could ignore C entirely and would not characterize a successor construction at all — the same underdetermination that sank the shell attempt.

No independence field beyond RankRepresentation's own, and no asserted equality between the two routes' outputs. AustinSuccessor and KallenbergSuccessor are the same proposition by construction (rfl), so whichever lands first discharges the induction step while the other stands as an independent proof of the same statement.

Regression status.

• Rank-zero / nullary — done: truncation_zero proves the truncation equation is automatic at rank zero, since the rank-zero latent cube is a single point and both sides are then determined by their structure marginals.
• Bipartite and i.i.d. — to come, in a separate shared regression module so this file stays interface-only. Both are to be genuinely adversarial: bipartite exhibiting a successor whose new singleton latents remain correlated with the array while truncating exactly to the old joint law; i.i.d. edges at rank 2 → 3, where truncation preserves independence from the old latents while the fresh edge latent makes the edge block recoverable.
• Mixed-pool — deliberately not a final-output regression here. RankSuccessor exposes no pooled carrier, so nothing at this interface could observe whether a proof actually used boundary-crossing permutations; such a check would be vacuous. That property is already formalized by the pooled gate's PooledRankExtension.map_restrict_embedding, which holds for every sortwise embedding, and each route's intermediate construction is required to consume it.

#196 remains open.

[cameronfreer]

Acceptance criteria for the two remaining shared regressions, pinned. Both live in a route-independent regression module; RelRankSuccessorContract.lean stays interface-only.

Bipartite, rank 1 → 2. Required witnesses:

• exact RankSuccessor truncation;
• an a.e. identity X_uv = z_u ⊕ z_v;
• a direct statement that the new latent family is not simply independent of the array over the old trivial layer.

I.i.d. edges, rank 2 → 3. Required witnesses:

• exact truncation;
• fair / nondegenerate edges given the old latents;
• explicit recovery of X_uv from the fresh support-{u,v} latent.

The second simultaneously tests staging and recovery.

Neither needs the strongest "no colour is graph-measurable" theorem. A concrete nonindependence identity for bipartite, and nondegeneracy plus fresh-coordinate decoding for i.i.d. edges, are sufficient acceptance tests.