feat: rank successor decomposition, unit 1 of the transition (#107)

Graphon.lean

@@ -27,6 +27,7 @@ import Graphon.RelRankOneTransfer
 import Graphon.RelFixingAlgebra
 import Graphon.RelRankAlgebra
 import Graphon.RelLowerFactor
+import Graphon.RelRankSuccessor
 import Graphon.RelRankOneCondIndep
 import Graphon.RelPollingInfrastructure
 import Graphon.RelFixingCondIndep
@@ -216,6 +217,7 @@ in Lean 4 using Mathlib.
 * `Graphon.RelStepKernel` — R4 converse piece 3 (#107): **one kernel per finite `A`**, `stepKernel A : Kernel (BoundarySpace A) (ExactSpace A)`, the conditional distribution of the exact-anchor layer given the whole proper-subset boundary — not one kernel per pair `C ⊆ A`, and not a chain. Built as `condDistrib`, whose standard-Borel hypothesis is exactly what the factor-space packaging supplies. Central identities: the disintegration `boundaryLaw A ⊗ₘ stepKernel A = M.law.map (boundaryMap A, exactMap A)`, marginal recovery `stepKernel A ∘ₘ boundaryLaw A = exactLaw A`, and the same read through `factorSpaceProdEquiv`. Valid for an arbitrary exchangeable law; the `A = ∅` base case is deliberately absent, since its determinism uses dissociation and belongs to the later realization layer
 * `Graphon.RelRankAlgebra` — R4 converse piece 3 (#107): the **lower-rank conditioning algebra** `lowerRankAlgebra n = ⨆ A, ⨆ (_ : A.card < n), fixingAlgebra A` and its order theory — monotone in the rank bound, below the ambient algebra, containing each low-rank fixing algebra, `⊥` at rank `0`, and `invariantAlgebra` at rank `1` (the recursion's base, and the reason no `NoNullary` hypothesis is needed). Plus `comap_relabel_lowerRankAlgebra`, invariance under an **arbitrary** sortwise permutation family — relabelings displacing infinitely many vertices arise naturally downstream, so the finite-support hypothesis would be too weak — and `card_inter_lt_of_ne`, that distinct supports of equal rank meet in strictly lower rank. Law-free throughout
 * `Graphon.RelLowerFactor` — R4 converse piece 3 (#107): the **structural lower-rank factor**, the object the rank recursion conditions on. `lowerFactorMap n` reads the coherent-basis coordinates whose anchor has cardinality `< n` into the standard Borel `LowerFactorSpace n`. It is stated about the *factor*, never about latents: a latent normally carries randomness beyond the factor it represents — already `1_{U < p}` generates strictly less than `U` — so a σ-algebra generated by latents is typically strictly larger. Generation is `comap (lowerFactorMap n) inferInstance ≤ lowerRankAlgebra n` together with an **eventwise** converse; no raw equality is asserted or supplied, the available converse being modulo `M.law`. The converse is proved support by support through `lowerToFactorProjection`, which exhibits `factorMap A` as a coordinate restriction whenever `A.card < n`, and the containments are joined inside `eventuallyMeasurableSpace` — already a σ-algebra, so the completion does the closing and no family of a.e. witnesses is ever chosen simultaneously through the `iSup`. `lowerIndexEquiv` gives `FinSuppPerm` equivariance as automorphisms of one fixed type (rank is preserved because anchors transport by an injective image map), so the action laws are honest equalities of equivalences with no dependent transport, and they commute with rank nesting definitionally. Rank `0` is `⊥` on the nose; rank `1` is the recursion's base, on the original law, with no augmented space and no coupling
+* `Graphon.RelRankSuccessor` — R4 converse piece 3 (#107), unit 1 of the rank transition `n → n+1`: the law-free structural split of the factor space into everything below rank `n` and the layer at rank exactly `n`. **The layer is a Bool-cube, not a dependent product**, and that is a load-bearing choice: `Π A : RankSupport S n, ExactSpace A` would force every downstream conditional law to be a kernel into a dependent product, and Mathlib has no countable dependent product of kernels — there is no `Kernel.pi`, the only `Π`-valued kernels being the Ionescu–Tulcea trajectory kernels, which are ℕ-indexed chains whose source is the history rather than a fixed common parameter. Since `ExactSpace A = ExactIndex A → Bool` the dependent product is already a Bool-cube on `{i // (anchor i).card = n}`, so `RankLayerIndex`/`RankLayerSpace`/`rankLayerMap` are defined directly that way, with `sigmaExactIndexEquiv` recording the bridge to the per-support view and `rankLayerMap_sigmaExactIndexEquiv` identifying each block with `exactMap A`. Downstream this means a layer conditional law is an ordinary `condDistrib` into a standard Borel space and mutual conditional independence supplies the finite products that finite-cylinder extensionality consumes — no product kernel anywhere. `lowerIndexSuccEquiv`/`lowerFactorSpaceSuccEquiv` give the split `LowerFactorSpace (n+1) ≃ᵐ LowerFactorSpace n × RankLayerSpace n`; `lowerToBoundaryProjection` reads the boundary at each rank-`n` support, definitionally compatible with `boundaryMap`. The relabeling actions `rankSupportEquiv`/`rankLayerIndexEquiv`/`rankLayerSpaceEquiv` are automorphisms of fixed types, so the action laws need no dependent transport; the square `lowerIndexSuccEquiv_rankLayerIndexEquiv` against the successor split is **not** definitional, since the split branches on `card < n` and the two sides' branch conditions agree only after transporting anchor cardinality through the image map. The **space-level** successor square `lowerFactorSpaceSuccEquiv_lowerFactorSpaceEquiv` *is* definitional, escaping the case split because it is built from `lowerIndexSuccEquiv.symm`, a `Sum.elim` that computes on the constructors. Per-support API for units 2 and 3: `rankLayerToExactProjection` (with `rankLayerToExactProjection_rankLayerMap` definitional), and the naturality squares for it, for `lowerToBoundaryProjection`, and for the support/exact bridge — all definitional, so per-support kernel identification and coherent randomization inherit them without transport bookkeeping
 * `Graphon.RelRankOneCondIndep` — R4 converse piece 3 (#107): the **rank-one mutual conditional independence**, `iCondIndepFun (fun v => exactMap {v}) invariantAlgebra M.law` — the singleton exact-anchor layers are mutually, not merely pairwise, conditionally independent given the invariant σ-algebra, for an arbitrary exchangeable law with no dissociation and no `NoNullary`. Proved entirely from the two-set `condIndep_fixingAlgebra` by peeling one vertex at a time: the accumulated events bundle into a single `fixingAlgebra s`-event by monotonicity, `{v} ∩ s = ∅`, so the two-set theorem conditions on `fixingAlgebra ∅ = invariantAlgebra` — the same algebra at every stage — and the products compose against the induction hypothesis. The peel is available *only* at rank one: for supports of rank `n > 1` the peeled support need not be disjoint from the accumulated union, and where it is not, that stage conditions on a larger algebra — and conditional independence is not preserved under enlarging the conditioning. A positive-rank intersection is not inevitable for every family, but it is possible, which is enough to break the induction. So no de Finetti representation, no mixing measure, and no identification of a mixing measure with an invariant conditional distribution is needed here
 * `Graphon.DigraphMaps` — the minimal `Digraph.comap` pullback API for Mathlib's `Digraph` (mirroring `SimpleGraph.comap`; a Mathlib-upstream candidate tracked on #24), used by the D2 directed-law bridge
 * `Graphon.InfiniteDigraphLaw` — Directed umbrella (#84) D2 (#86): the `PMF`-based finite directed law `ExchangeableDigraphLaw` (consistent under `Digraph.comap`), the finite bridge `digraphLawEquiv : ExchangeableDigraphLaw ≃ RelExchangeableLaw digraphSig` (via `finiteDigraphEquiv` + `PMF.toMeasure`/`Measure.toPMF`), and the headline `exchangeableDigraphLawEquiv : ExchangeableDigraphLaw ≃ InfiniteExchangeableDigraphLaw` composing with R2c — measurable structure stays on the relational carrier

Graphon/RelLowerFactor.lean

@@ -227,28 +227,20 @@ theorem exists_comap_lowerFactorMap_ae_eq (n : ℕ)
 
 /-! ### Equivariance -/
 
-private theorem sigmaMap_inj (σ : FinSuppPerm S) :
-    Function.Injective (Sigma.map id fun s => ⇑(σ.1 s) :
-      (Σ s : S.Srt, Vinfinite S s) → Σ s : S.Srt, Vinfinite S s) := by
-  have hinv : Function.LeftInverse
-      (Sigma.map id fun s => ⇑((σ⁻¹ : FinSuppPerm S).1 s) :
-        (Σ s : S.Srt, Vinfinite S s) → Σ s : S.Srt, Vinfinite S s)
-      (Sigma.map id fun s => ⇑(σ.1 s)) := by
-    rintro ⟨s, x⟩
-    show (⟨s, (σ⁻¹ : FinSuppPerm S).1 s (σ.1 s x)⟩ : Σ s : S.Srt, Vinfinite S s) = ⟨s, x⟩
-    rw [show (σ⁻¹ : FinSuppPerm S).1 s (σ.1 s x) = x from (σ.1 s).symm_apply_apply x]
-  exact hinv.injective
-
 open scoped Classical in
 /-- **A relabeling as an equivalence of the lower-rank index.** Unlike `basisIndexEquiv`, this
 is an equivalence of a *single* type: a relabeling transports anchors by an injective image map,
 so it preserves cardinality and hence rank. -/
 noncomputable def lowerIndexEquiv (σ : FinSuppPerm S) (n : ℕ) :
     B.LowerIndex n ≃ B.LowerIndex n where
   toFun i := ⟨B.act σ i.1, by
-    rw [B.anchor_act, Finset.card_image_of_injective _ (sigmaMap_inj σ)]; exact i.2⟩
+    rw [B.anchor_act, Finset.card_image_of_injective _
+      (Function.injective_id.sigma_map fun s => (σ.1 s).injective)]
+    exact i.2⟩
   invFun j := ⟨B.act σ⁻¹ j.1, by
-    rw [B.anchor_act, Finset.card_image_of_injective _ (sigmaMap_inj σ⁻¹)]; exact j.2⟩
+    rw [B.anchor_act, Finset.card_image_of_injective _
+      (Function.injective_id.sigma_map fun s => ((σ⁻¹ : FinSuppPerm S).1 s).injective)]
+    exact j.2⟩
   left_inv i := Subtype.ext (by
     show B.act σ⁻¹ (B.act σ i.1) = i.1
     rw [← B.act_mul, inv_mul_cancel, B.act_one])

Graphon/RelRankAlgebra.lean

@@ -93,19 +93,6 @@ theorem RelStructure.lowerRankAlgebra_one :
 
 /-! ### Invariance under relabeling -/
 
-open scoped Classical in
-private theorem sigmaMap_injective (σ : ∀ _ : S.Srt, Equiv.Perm ℕ) :
-    Function.Injective (Sigma.map id fun s => ⇑(σ s) :
-      (Σ s : S.Srt, Vinfinite S s) → Σ s : S.Srt, Vinfinite S s) := by
-  have hinv : Function.LeftInverse
-      (Sigma.map id fun s => ⇑(σ s)⁻¹ :
-        (Σ s : S.Srt, Vinfinite S s) → Σ s : S.Srt, Vinfinite S s)
-      (Sigma.map id fun s => ⇑(σ s)) := by
-    rintro ⟨s, x⟩
-    show (⟨s, (σ s)⁻¹ (σ s x)⟩ : Σ s : S.Srt, Vinfinite S s) = ⟨s, x⟩
-    rw [show (σ s)⁻¹ (σ s x) = x from (σ s).symm_apply_apply x]
-  exact hinv.injective
-
 open scoped Classical in
 private theorem image_image_inv_rank (σ : ∀ _ : S.Srt, Equiv.Perm ℕ)
     (A : Finset (Σ s : S.Srt, Vinfinite S s)) :
@@ -140,9 +127,11 @@ theorem RelStructure.comap_relabel_lowerRankAlgebra [Fintype S.Srt]
     RelStructure.fixingAlgebra_comap_relabel_of_fintype σ]
   refine le_antisymm (iSup₂_le fun A hA => ?_) (iSup₂_le fun A hA => ?_)
   · exact le_iSup₂_of_le (A.image (Sigma.map id fun s => ⇑(σ s)))
-      (by rwa [Finset.card_image_of_injective _ (sigmaMap_injective σ)]) le_rfl
+      (by rwa [Finset.card_image_of_injective _
+        (Function.injective_id.sigma_map fun s => (σ s).injective)]) le_rfl
   · refine le_iSup₂_of_le (A.image (Sigma.map id fun s => ⇑(σ s)⁻¹))
-      (by rwa [Finset.card_image_of_injective _ (sigmaMap_injective fun s => (σ s)⁻¹)])
+      (by rwa [Finset.card_image_of_injective _
+        (Function.injective_id.sigma_map fun s => ((σ s)⁻¹).injective)])
       (le_of_eq ?_)
     rw [image_image_inv_rank σ A]