feat: i.i.d.-edge regression for the successor contract (#196)

Graphon.lean

@@ -49,7 +49,9 @@ import Graphon.RelPooledLatents
 import Graphon.RelPooledExtension
 import Graphon.RelPooledAcceptance
 import Graphon.RelRankSuccessorContract
+import Graphon.DigraphCoordSupport
 import Graphon.RelBipartiteRegression
+import Graphon.RelIidEdgeRegression
 import Graphon.RelSingletonPeel
 import Graphon.RelFixingAlgebra
 import Graphon.RelRankAlgebra
@@ -270,7 +272,9 @@ in Lean 4 using Mathlib.
 * `Graphon.RelPooledExtension` — R4 converse (#107), stage 2 of the pooled-latent extension gate: **the pooled rank extension**. `PooledRankExtension C` carries exactly three fields — the joint law on the pooled structure space times the pooled latent cube, its exact restriction to `C.P` along the two original restrictions, and invariance under the **full** pooled permutation family (mixed permutations included, the load-bearing quantifier). **No independence field**: an independent pool would recreate the defect of the rejected factor coupling. `RankRepresentation.pooledExtension` is the cheap constructor, and both of its laws are `map_prodMap_restrict_self` in disguise — writing `pv` for `poolVertexEquiv` and `ov` for `originalVertex`, the transport is `comap pv` on structures and restriction along `pv` on latents; `restrictOriginal ∘ transport` is `comap (pv ∘ ov)` with `pv ∘ ov` a **self-injection** of the original carrier, and `relabel ρ ∘ transport = transport ∘ relabel κ` for the conjugate `κ = pv ∘ ρ ∘ pv⁻¹`, a **permutation** of it. The structure deliberately carries **no mixed-window field**: the joint mixed-window marginal, and current-rank recovery and screening on mixed pooled supports, are separate derived consequences of the three fields rather than part of the primitive, and nothing route-specific belongs here
 * `Graphon.RelPooledAcceptance` — R4 converse (#107), stage 3 of the pooled-latent extension gate, organizing result: **the joint restriction theorem**. For *every* sortwise embedding `e : ∀ s, Vinfinite S s ↪ PoolVertex S s`, restricting a pooled rank extension jointly — structure and latents along the same embedding — returns the representation exactly: `Q.law.map (Prod.map (RelStructure.restrict e) (latentRestrictOver e n)) = C.P`. Being **joint** is the point: it recovers the `(X, U_{<n})` law and says strictly more than a structure-only window theorem. Proved by joint-cylinder extensionality plus finite agreement with a mixed pooled permutation — on a cylinder the combined vertex support is finite, the assignment `originalVertex v ↦ e v` there is a finite partial injection of the pooled carrier, and `exists_perm_extend_of_injOn` extends it; the full mixed invariance then absorbs the permutation, which is also what lets it be chosen independently on each sort with no finite-support or uniform-bound issue. The four route-neutral consequences follow from it: `map_snd` (the pooled latent marginal is the pooled i.i.d. source), `toStationaryExtension` (the structure marginal is a `StationaryExtension M`), `lower_recovers` (local recovery on every pooled support below rank `n`, the decoder conjugated through the local and block measurable equivalences), and `screening` (screening on every pooled support of rank `n`, a pullback through `measurePreserving_pooledJointEquiv` followed by `CondIndepFun.comp` on the codomains and `CondIndepFun.congr_cond` with `comap_measurableEquiv_comp` on the conditioning algebra — no conditional-expectation reasoning). `PooledRankExtension.map_poolVertexEquiv` is the canonical specialization; bundling that restriction as the measurable equivalence `pooledJointEquiv` and cancelling it yields **`PooledRankExtension.law_eq`, a uniqueness theorem** — every pooled rank extension *is* the cheap one. Marginals, the `StationaryExtension` structure, recovery and screening therefore transport from `C.P` through one canonical law identity rather than requiring separate measure arguments
 * `Graphon.RelRankSuccessorContract` — R4 converse (#107), **interface only**: the shared witness both successor constructions must produce, and the two identically typed statements they target. `RankSuccessor C` carries the next representation together with **exact truncation compatibility**, `next.P.map (Prod.map id (rankLatentProjection (Nat.le_succ n))) = C.P` — the observable that makes the statement mention `C` at all. A theorem returning merely `Nonempty (RankRepresentation (n + 1))` could ignore `C` and produce an unrelated representation, which is the same underdetermination that sank the earlier shell attempt. The witness carries **no independence field** beyond `RankRepresentation`'s own, and **no equality between the two routes' outputs** is asserted — they prove one statement by different means and will not produce canonically equal representations. `AustinSuccessor` and `KallenbergSuccessor` are the same proposition by construction, so whichever lands first discharges the induction while the other remains an independent proof. Regression: `truncation_zero` shows the truncation equation is **automatic at rank zero** — the rank-zero latent cube is a single point, so both sides are determined by their structure marginals, which the representation axioms already pin, and the base case imposes nothing extra. The witness exposes no pooled carrier, so whether a construction genuinely used boundary-crossing permutations is observed by the pooled gate's `map_restrict_embedding` rather than by any final-output check here; each route's intermediate construction consumes that theorem. Adversarial examples are kept in route-independent regression modules, outside this interface
+* `Graphon.DigraphCoordSupport` — shared regression infrastructure: the support of a digraph coordinate is the pair of its endpoints, with the off-diagonal cardinality corollary, over an arbitrary vertex type. A bridge module so that the D1 carrier `Graphon.InfiniteDigraph` does not acquire a dependency on the equality-pattern layer where `RelCoord.support` lives — the same separation `Graphon.SimpleGraphDigraphBridge` maintains for `SimpleGraph`. Stated with `[DecidableEq V]` and proved by membership, because `RelCoord.support` is built classically and over a concrete carrier the natural instance is not definitionally the classical one, so an image-shaped statement would not apply at the sites that need it
 * `Graphon.RelBipartiteRegression` — R4 converse (#107/#196): the **bipartite regression** for the successor contract, a hand-built rank `1 → 2` witness over `digraphSig` whose purpose is to test that `RankSuccessor` is an expressive specification *before* either route is attempted. Each vertex carries an i.i.d. colour on its own fresh singleton coordinate and the edge is the parity, so the diagonal is constantly `false` for free. Three independent things make it a regression rather than a construction: the array law is defined **from the fresh singleton layer alone** and the rank-one coupling as the independent product `bipartiteLaw × rankLatentSource 1`, so `rankTwoCoupling_truncation` compares two separately described couplings and genuinely consumes the source factorization; the rank-two block decoder recovers **both** directed coordinates `X_uv` and `X_vu` as the same parity, exhibiting symmetry as a property of this law rather than of the signature; and `not_indepFun_rankTwoCoupling` is **numerical** — the edge and colour-parity events coincide with probability `1/2` against a product of marginals `1/4`, which a constant edge could not achieve even though it too would be "a function of the colours". `bipartiteSuccessor : RankSuccessor rankOneRep` is the witness itself
+* `Graphon.RelIidEdgeRegression` — R4 converse (#107/#196): the **i.i.d.-edge regression** for the successor contract, a hand-built rank `2 → 3` witness over `digraphSig` that tests **staging and recovery** where the bipartite regression tested independence and symmetry. The array is keyed by a coordinate's *support*, which gives symmetry (`X_uv = X_vu`) and the empty diagonal by construction — each is still proved from a support computation, but neither requires a choice of orientation. Two things make it a regression rather than a construction. First, recovery is genuinely staged: at rank three a two-point block is decoded from the latent coordinate at its own support — carried by the rank-three array because `2 < 3` — while at rank two the same blocks are not latent-measurable at all, so the two ranks exercise opposite sides of `lower_recovers`. Second, rank-two screening is a genuine conditional-independence statement: the block reads one coordinate of the edge source and the remainder reads the others plus the whole latent array, so screening follows from **independence**, not from determinism as in the bipartite case. `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly `1/2`, which rules out a *constant* block; that the block is not measurable from the old latents is a separate fact, supplied by the product independence built into the rank-two coupling. The private conditional-independence lemma is stated for abstract σ-algebras rather than for the two coordinates of a product because the ambient measure is a pushforward of a product and the current API only transports conditional independence **backward**: a source-level proof would require a new forward law-transport theorem, whereas transporting the unconditional independence needs no new theorem. `iidEdgeSuccessor : RankSuccessor rankTwoRep` is the witness itself
 * `Graphon.RelRankInjectionInvariance` — R4 converse (#107), the isolated proof risk of the pooled-latent extension gate: **joint invariance under arbitrary sortwise self-injections**. `RankRepresentation.invariant` is stated for *finitely supported permutations*, but a pooled object built cheaply through `poolVertexEquiv` needs the joint law invariant under every self-injection; `RankRepresentation.map_prodMap_restrict_self` supplies exactly that, so full mixed pooled invariance later costs no additional mathematics. The route is finite-cylinder extensionality on the **joint** space, which had no machinery before — rank one's joint invariance goes through only because the rank-one latent action is trivial. `rankLatentIndexInj`/`rankLatentReindex` extend the latent action from permutations to injections (only injectivity is used — a support keeps its cardinality); `exists_finSuppPerm_agree_on_finset` matches an injection to a finitely supported permutation on any finite tagged-vertex support; `ext_of_prod_cylinders` is the joint extensionality, rectangles of coordinate cylinders on both factors. **No finiteness/`Fintype` hypothesis beyond `RankRepresentation`'s ambient countability.** Equality is tested on *coordinate* cylinders — finitely many `RelCoord`s and finitely many latent indices — whose combined vertex support is one finite `Finset (Σ s, Vinfinite S s)` and so touches only finitely many sorts; the injection is matched there by extending it on each active sort, taking the identity elsewhere, and maximizing finitely many support bounds. The coarser `restrictFin` cylinder family would instead force a uniform all-sort bound that no self-injection need admit
 * `Graphon.RelRankCoding` — R4 converse piece 3 (#107): factor-law coding of the lower-rank factor. **Not** the inductive hypothesis of a working recursion: `RankCoding n → ShellProperty n` is **false**, refuted by Austin's random complete bipartite graph `X_uv = z_u ⊕ z_v` (arXiv:0801.1698 §3.6), where `lowerRankAlgebra 2` is trivial modulo the law but every triangle satisfies `X₁₂ ⊕ X₁₃ ⊕ X₂₃ = 0`, so the exact layers are pairwise but not mutually independent — while a `RankCoding 2` exists because the rank-2 factor law is a point mass. The example separates the true two-set theorem from mutuality, and shows the gap is not closable by coupling: a relatively independent joining over `lowerFactorMap` attaches latents that are conditionally independent of the structure given a trivial factor, whereas a representation needs the hidden colours, correlated with the array yet not recoverable from it. `RankCoding n` represents the rank-`n` factor by latents — a measurable coding map carrying the latent source to the factor law and intertwining the two relabeling actions **almost everywhere**. The a.e. form is forced: `lowerFactorSpaceEquiv σ n` fixes the *image* of `lowerFactorMap n`, not the whole Bool-cube, since it permutes distinct basis indices that name the same event, so the strict version is false already at rank one. `ShellProperty n` is the conclusion the recursion consumes, bundling mutual conditional independence of the exact layers over the rank-`n` supports **with** per-support locality; neither half implies the other, since mutual independence given the whole lower-rank factor permits dependence on all of it rather than only through `boundaryMap A`. `RankCoding.rankOne` is the base case, built from the #140 randomization adapter transported along `rankLatentOneEquiv`; its equivariance clause is genuinely exercised rather than vacuous, because at rank one the latent relabeling is the identity while the factor equivalence is not
 * `Graphon.RelFixingAlgebra` — R4 converse piece 2a (#107): the **law-independent** factor-algebra layer — `SortwiseFixing` (the `A`-fixing stabilizer of finitely supported sortwise permutations, closed under `1`/`*`/`⁻¹`/conjugation), the raw `RelStructure.fixingAlgebra` (events invariant under the `A`-fixing group; deliberately *not* "generated by relations inside `A`", which loses hidden vertex information), monotonicity, `fixingAlgebra_empty = invariantAlgebra` (near-definitional), and the **transport equality** `fixingAlgebra_comap_relabel : comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (image σ A)` via stabilizer conjugation — no completions, no law; the conditional-independence theorem is its own later PR

Graphon/DigraphCoordSupport.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Cameron Freer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Cameron Freer
+-/
+import Graphon.InfiniteDigraph
+import Graphon.RelEqualityPattern
+
+/-!
+# Support geometry of digraph coordinates (shared regression infrastructure)
+
+The support of a digraph coordinate, in its own module so that the foundational relational/directed
+carrier `Graphon.InfiniteDigraph` (D1) does not depend on the equality-pattern layer
+`Graphon.RelEqualityPattern`, where `RelCoord.support` is defined. Every D1 consumer would
+otherwise inherit that dependency for the sake of two lemmas neither it nor they use — the same
+reason `Graphon.SimpleGraphDigraphBridge` keeps `SimpleGraph` out of D1.
+
+Both regressions for the R4 successor contract (#196) were proving this geometry independently;
+it is stated here once, over an arbitrary vertex type.
+
+The pair is stated with `[DecidableEq V]` and proved by **membership** rather than by unfolding an
+image. That is not a stylistic choice: `RelCoord.support` is built with the classical instance, and
+over a concrete carrier the natural `DecidableEq` is not definitionally equal to it, so an
+image-shaped statement would be unusable at exactly the sites that need it.
+-/
+
+open RelSignature
+
+open scoped Classical in
+/-- **The support of a digraph coordinate** is the pair of its endpoints. Proved by membership, so
+that the `DecidableEq` instance forming the pair is the caller's rather than the classical one used
+to build `RelCoord.support`. -/
+theorem support_digraphCoord {V : Type*} [DecidableEq V] (a b : V) :
+    (digraphCoord a b : RelCoord digraphSig (fun _ => V)).support =
+      {(⟨(), a⟩ : Σ _ : Unit, V), ⟨(), b⟩} := by
+  refine Finset.ext fun w => ?_
+  rw [RelCoord.mem_support_iff]
+  simp only [Finset.mem_insert, Finset.mem_singleton]
+  constructor
+  · rintro ⟨i, rfl⟩
+    fin_cases i
+    · exact Or.inl rfl
+    · exact Or.inr rfl
+  · rintro (rfl | rfl)
+    · exact ⟨0, rfl⟩
+    · exact ⟨1, rfl⟩
+
+/-- **An off-diagonal digraph coordinate has a two-point support.** -/
+theorem card_support_digraphCoord {V : Type*} [DecidableEq V] {a b : V} (hab : a ≠ b) :
+    (digraphCoord a b : RelCoord digraphSig (fun _ => V)).support.card = 2 := by
+  rw [support_digraphCoord]
+  exact Finset.card_pair fun h => hab (congrArg Sigma.snd h)