feat: shared successor contract, interface only (#196)

[cameronfreer]

The shared successor contract for #196 — interface only, no construction, no route implementation.

The witness

structure RankSuccessor (C : M.RankRepresentation n) where
  next : M.RankRepresentation (n + 1)
  truncation : next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P

Exact law-level truncation is the essential observable. A theorem returning merely Nonempty (M.RankRepresentation (n + 1)) could ignore C entirely and produce an unrelated rank-(n+1) representation — it would not characterize a successor construction at all, which is the same underdetermination that sank the earlier shell attempt. The compatibility is therefore a field, exactly and not almost-everywhere.

What it deliberately omits

• No independence field beyond what RankRepresentation already states.
• No equality between the two routes' outputs. AustinSuccessor and KallenbergSuccessor are the same proposition by construction (austinSuccessor_eq_kallenbergSuccessor is rfl), so whichever route lands first discharges the induction step while the other stands as an independent proof of the same statement. Their witnesses will not be canonically equal and nothing here says otherwise.
• No pool. RankSuccessor exposes no pooled carrier, so no final-output regression here could observe whether a proof used boundary-crossing permutations; such a check would be vacuous. That property is formalized by the pooled gate's PooledRankExtension.map_restrict_embedding (feat: pooled-latent gate stage 3 — joint restriction, law identity, and the four consequences (#195) #201), and each route's intermediate construction is required to consume it — recorded as a requirement on R4 successor route A (Austin): polling → enriched object → kernel → noise outsourcing (#107) #197 and R4 successor route B (Kallenberg): direct correlated subset latents — independent check (#107) #198 that the dependency appear in the proof term rather than in prose.

The statements are Prop-valued definitions rather than unproved theorems, so the file is sorry-free while stating targets it does not prove.

Regression included

truncation_zero — the truncation equation is automatic at rank zero: the rank-zero latent index type is empty, so the cube is a single point, both sides are determined by their structure marginals, and RankRepresentation.map_fst pins those to M.law. The base case imposes nothing beyond the representation axioms.

The two adversarial regressions (bipartite rank 1 → 2, i.i.d. edges rank 2 → 3) land as their own PRs in a route-independent module, keeping this file interface-only and free of their heavier imports. Both must construct C independently rather than as a projection of D, so that truncation compares two separately described couplings instead of holding tautologically.

Bookkeeping

• New module Graphon/RelRankSuccessorContract.lean; import and doc bullet in Graphon.lean.
• Audit 407 → 409 in both scripts/axiom_audit.lean and the intended-set literal in scripts/check_census_and_axioms.py.
• Gates: lake build clean (3404 jobs), census + axiom audit pass, zero sorries.