The successor contract (R4 converse, #107)

Interface only: the shared witness type that both successor constructions must produce, and the two identically typed statements they target. No construction is performed here.

Why a witness type rather than Nonempty (RankRepresentation (n + 1))

A theorem returning merely Nonempty (M.RankRepresentation (n + 1)) does not characterize a successor construction at all: it could ignore C entirely and produce an unrelated rank-(n+1) representation. That is the same kind of underdetermined contract that caused the earlier failure, so the compatibility is made an explicit observable:

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

Truncating the successor's latents back to rank n returns C.P on the nose — exactly, not almost everywhere and not up to isomorphism.

What the witness deliberately does not carry

• No independence field beyond what RankRepresentation already states — recovery and screening at the working rank are fields of next itself, and nothing further is asserted.
• No equality between the two routes' outputs. They prove the same existence statement by different means and will not produce canonically equal representations; asserting otherwise would be false. The public induction may cite whichever lands first, and the other remains an independently audited proof path.
• No pool. RankSuccessor exposes no pooled carrier, so no final-output regression here could observe whether a proof actually used boundary-crossing permutations. That property is already formalized by the pooled gate's joint restriction theorem for every sortwise embedding (PooledRankExtension.map_restrict_embedding); each route's intermediate construction is required to consume it, rather than a vacuous check being added at this interface.

Adversarial examples are kept in route-independent regression modules, outside this interface, so that this file stays interface-only and free of the heavier imports they need.

structure RelSignature.InfiniteRelExchangeableLaw.RankSuccessor {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} {n : ℕ} (C : M.RankRepresentation n) : Type u_1

A successor witness: a rank-(n+1) representation whose latent truncation returns the given rank-n representation exactly. This is what both routes must produce.

• next : M.RankRepresentation (n + 1)

  The next representation.

• truncation : MeasureTheory.Measure.map (Prod.map id (rankLatentProjection ⋯)) self.next.P = C.P

  Exact truncation compatibility: forgetting the fresh rank-n latent layer returns C.P on the nose. Without this the statement would not mention C at all.

theorem RelSignature.InfiniteRelExchangeableLaw.RankSuccessor.measurable_truncation {S : RelSignature} [Countable S.Srt] {n : ℕ} : Measurable (Prod.map id (rankLatentProjection ⋯))

The truncation map is measurable, so the witness's identity is an identity of pushforwards along a measurable map.

Regression: the rank-zero base

At rank zero the latent cube is a single point — there is no support of cardinality below 0 — so the truncation observable degenerates exactly as it should: it constrains only the structure marginal, which RankRepresentation already pins. This records why the base case imposes nothing extra, and it is the first of the shared regressions the contract must survive.

instance RelSignature.InfiniteRelExchangeableLaw.instIsEmptyRankLatentIndexOfNatNat {S : RelSignature} : IsEmpty (S.RankLatentIndex 0)

instance RelSignature.InfiniteRelExchangeableLaw.instSubsingletonRankLatentSpaceOfNatNat {S : RelSignature} : Subsingleton (S.RankLatentSpace 0)

@[implicit_reducible]

instance RelSignature.InfiniteRelExchangeableLaw.instUniqueRankLatentSpaceOfNatNat {S : RelSignature} : Unique (S.RankLatentSpace 0)

Equations

• RelSignature.InfiniteRelExchangeableLaw.instUniqueRankLatentSpaceOfNatNat = Pi.uniqueOfIsEmpty fun (a : S.RankLatentIndex 0) => ℝ

theorem RelSignature.InfiniteRelExchangeableLaw.truncation_zero {S : RelSignature} [Countable S.Srt] [Countable S.Rel] {M : S.InfiniteRelExchangeableLaw} (C : M.RankRepresentation 0) (D : M.RankRepresentation 1) : MeasureTheory.Measure.map (Prod.map id (rankLatentProjection ⋯)) D.P = C.P

The truncation equation is automatic at rank zero. For any rank-zero and rank-one representations of the same law, truncation holds — the rank-zero latent cube is a single point, so both sides are determined by their structure marginals, which RankRepresentation.map_fst already pins to M.law. The base case therefore imposes nothing beyond the representation axioms.

def RelSignature.InfiniteRelExchangeableLaw.SuccessorStatement (S : RelSignature) [Countable S.Srt] [Countable S.Rel] : Prop

The successor statement, as a proposition: every rank-n representation admits a successor witness. Both routes target this exact statement, and neither is proved here.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev RelSignature.InfiniteRelExchangeableLaw.KallenbergSuccessor (S : RelSignature) [Countable S.Srt] [Countable S.Rel] : Prop

The Kallenberg route's target: the shared successor statement, reached by directly constructing the correlated subset latents. Stated here, proved in its own unit.

Equations

• RelSignature.InfiniteRelExchangeableLaw.KallenbergSuccessor S = RelSignature.InfiniteRelExchangeableLaw.SuccessorStatement S

@[reducible, inline]

abbrev RelSignature.InfiniteRelExchangeableLaw.AustinSuccessor (S : RelSignature) [Countable S.Srt] [Countable S.Rel] : Prop

The Austin route's target: the shared successor statement, reached through polling, an enriched lower-rank object, a conditional kernel, and noise outsourcing. Stated here, proved in its own unit.

Equations

• RelSignature.InfiniteRelExchangeableLaw.AustinSuccessor S = RelSignature.InfiniteRelExchangeableLaw.SuccessorStatement S

theorem RelSignature.InfiniteRelExchangeableLaw.austinSuccessor_eq_kallenbergSuccessor (S : RelSignature) [Countable S.Srt] [Countable S.Rel] : AustinSuccessor S = KallenbergSuccessor S

The two route targets are the same proposition — by construction, not by an asserted identification of their outputs. Whichever is proved first discharges the induction step; the other remains an independent proof of the same statement.