From 2125203dcec2d972cb24cc700649d7c19d7bb1ba Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 17 Aug 2026 03:28:45 +0000
Subject: [PATCH 01/11] wip(#196): bipartite law and the independently-defined
 rank-one representation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The XOR array over digraphSig: each vertex carries an i.i.d. colour on
its own fresh singleton coordinate, and the edge is the parity. The
diagonal is constantly false for free, since b XOR b = false.

bipartiteLaw is defined from the FRESH SINGLETON LAYER ALONE — not read
off any rank-two object — with exchangeability from the equivariance
arr (ω ∘ supportPerm σ) = relabel σ (arr ω) plus source invariance under
an index equivalence.

rankOneRep : RankRepresentation 1 with P := bipartiteLaw.prod
(rankLatentSource 1), the independent product. Its invariance uses the
rank-one latent action being the identity; lower_recovers is trivial
because no coordinate of this signature has empty support, so the
rank-zero block space is a point; screening is condIndepFun_const_left
transported by CondIndepFun.congr, since the singleton block reads only
the constantly-false diagonal.
---
 Graphon/RelBipartiteRegression.lean | 277 ++++++++++++++++++++++++++++
 1 file changed, 277 insertions(+)
 create mode 100644 Graphon/RelBipartiteRegression.lean

diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
new file mode 100644
index 0000000..ebcfde1
--- /dev/null
+++ b/Graphon/RelBipartiteRegression.lean
@@ -0,0 +1,277 @@
+/-
+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.RelRankSuccessorContract
+import Graphon.InfiniteDigraph
+import Graphon.ForMathlib.CondIndepSup
+
+/-!
+# The bipartite regression for the successor contract (R4 converse, #107)
+
+A hand-built rank `1 → 2` successor witness for the one-sort binary signature `digraphSig`, whose
+purpose is to test that `RankSuccessor` is an expressive specification — **before** either general
+route is attempted, so that the acceptance battery cannot be shaped by an implementation.
+
+The array is the bipartite XOR law: each vertex carries an i.i.d. colour, and the edge `X_uv` is
+the parity `colour u ⊕ colour v`.
+
+## What makes this a regression rather than merely a construction
+
+* the array law `bipartiteLaw` is defined **from the fresh singleton layer alone**, and the
+  rank-one coupling `C` is defined as the independent product `bipartiteLaw × rankLatentSource 1`.
+  Neither is read off the rank-two coupling, so the truncation identity compares two separately
+  described couplings and genuinely uses the source factorization;
+* the nonindependence witness is **numerical**, not merely functional: `X_01` and the matching
+  colour-parity event have joint probability `1/2` against a product of marginals `1/4`. "The edge
+  is a function of the colours" would also hold for a constant edge and would certify nothing;
+* the rank-two decoder recovers **both** directed coordinates `X_uv` and `X_vu` of the
+  support-`{u,v}` block as the same parity, so symmetry is exhibited as a property of this law
+  rather than something hidden in the signature. The diagonal singleton block is constantly
+  `false`, which the XOR definition delivers for free.
+-/
+
+open MeasureTheory ProbabilityTheory
+
+namespace RelSignature
+
+namespace BipartiteRegression
+
+/-- The fresh singleton layer of the rank-two latent cube: one uniform per vertex. -/
+abbrev Colours := RankSupport digraphSig 1 → ℝ
+
+/-- The singleton support at a vertex. -/
+def vertexSupport (v : ℕ) : RankSupport digraphSig 1 :=
+  ⟨{⟨(), v⟩}, Finset.card_singleton _⟩
+
+/-- The colour of a vertex, read off its own fresh coordinate. -/
+noncomputable def colour (ω : Colours) (v : ℕ) : Bool := decide (ω (vertexSupport v) ≤ 1 / 2)
+
+/-- **The bipartite array**: the edge at an ordered pair is the parity of the two colours. The
+diagonal is constantly `false` because `b ⊕ b = false`. -/
+noncomputable def arr (ω : Colours) : RelStructure digraphSig (Vinfinite digraphSig) :=
+  fun c => xor (colour ω (c.2 0)) (colour ω (c.2 1))
+
+@[simp] theorem arr_apply (ω : Colours) (u v : ℕ) :
+    arr ω (digraphCoord u v) = xor (colour ω u) (colour ω v) := rfl
+
+/-- **The diagonal is constantly false** — the singleton-support block of this law carries no
+information, which is what makes its rank-one recovery and screening deterministic. -/
+@[simp] theorem arr_diagonal (ω : Colours) (v : ℕ) : arr ω (digraphCoord v v) = false := by
+  simp [arr_apply, Bool.xor_self]
+
+theorem measurable_colour (v : ℕ) : Measurable fun ω : Colours => colour ω v := by
+  refine measurable_to_countable' fun b => ?_
+  cases b
+  · have hpre : (fun ω : Colours => colour ω v) ⁻¹' {false}
+        = {ω : Colours | ω (vertexSupport v) ≤ 1 / 2}ᶜ := by
+      ext ω; simp [colour]
+    rw [hpre]
+    exact (measurableSet_le (measurable_pi_apply _) measurable_const).compl
+  · have hpre : (fun ω : Colours => colour ω v) ⁻¹' {true}
+        = {ω : Colours | ω (vertexSupport v) ≤ 1 / 2} := by
+      ext ω; simp [colour]
+    rw [hpre]
+    exact measurableSet_le (measurable_pi_apply _) measurable_const
+
+theorem measurable_arr : Measurable arr := by
+  refine measurable_pi_lambda _ fun c => ?_
+  exact (Measurable.of_discrete (f := fun p : Bool × Bool => xor p.1 p.2)).comp
+    ((measurable_colour (c.2 0)).prodMk (measurable_colour (c.2 1)))
+
+/-! ### The relabeling action on the fresh layer -/
+
+open scoped Classical in
+/-- A permutation of the vertices permutes the singleton supports. -/
+noncomputable def supportPerm (σ : Equiv.Perm ℕ) :
+    RankSupport digraphSig 1 ≃ RankSupport digraphSig 1 where
+  toFun A := ⟨A.1.image (Sigma.map id fun _ => ⇑σ), by
+    rw [Finset.card_image_of_injective _
+      (Function.injective_id.sigma_map fun _ => σ.injective)]
+    exact A.2⟩
+  invFun A := ⟨A.1.image (Sigma.map id fun _ => ⇑σ.symm), by
+    rw [Finset.card_image_of_injective _
+      (Function.injective_id.sigma_map fun _ => σ.symm.injective)]
+    exact A.2⟩
+  left_inv A := Subtype.ext (by
+    show (A.1.image (Sigma.map id fun _ => ⇑σ)).image (Sigma.map id fun _ => ⇑σ.symm) = A.1
+    rw [Finset.image_image]
+    refine (Finset.image_congr fun v _ => ?_).trans A.1.image_id
+    obtain ⟨s, x⟩ := v
+    show (⟨s, σ.symm (σ x)⟩ : Σ _ : Unit, ℕ) = ⟨s, x⟩
+    rw [σ.symm_apply_apply])
+  right_inv A := Subtype.ext (by
+    show (A.1.image (Sigma.map id fun _ => ⇑σ.symm)).image (Sigma.map id fun _ => ⇑σ) = A.1
+    rw [Finset.image_image]
+    refine (Finset.image_congr fun v _ => ?_).trans A.1.image_id
+    obtain ⟨s, x⟩ := v
+    show (⟨s, σ (σ.symm x)⟩ : Σ _ : Unit, ℕ) = ⟨s, x⟩
+    rw [σ.apply_symm_apply])
+
+open scoped Classical in
+@[simp] theorem supportPerm_vertexSupport (σ : Equiv.Perm ℕ) (v : ℕ) :
+    supportPerm σ (vertexSupport v) = vertexSupport (σ v) := by
+  refine Subtype.ext ?_
+  show ({(⟨(), v⟩ : Σ _ : Unit, ℕ)} : Finset _).image (Sigma.map id fun _ => ⇑σ)
+    = ({⟨(), σ v⟩} : Finset (Σ _ : Unit, ℕ))
+  rw [Finset.image_singleton]
+  rfl
+
+theorem colour_comp_supportPerm (σ : Equiv.Perm ℕ) (ω : Colours) (v : ℕ) :
+    colour (fun A => ω (supportPerm σ A)) v = colour ω (σ v) := by
+  simp [colour]
+
+/-- **Equivariance of the array**: relabeling the vertices is reindexing the fresh layer. -/
+theorem arr_comp_supportPerm (σ : Equiv.Perm ℕ) (ω : Colours) :
+    arr (fun A => ω (supportPerm σ A)) =
+      RelStructure.relabel (fun _ : Unit => σ) (arr ω) := by
+  funext c
+  show xor (colour (fun A => ω (supportPerm σ A)) (c.2 0))
+      (colour (fun A => ω (supportPerm σ A)) (c.2 1)) = _
+  rw [colour_comp_supportPerm, colour_comp_supportPerm]
+  rfl
+
+/-! ### The array law -/
+
+/-- **The bipartite law**, defined from the fresh singleton layer alone — deliberately *not* read
+off the rank-two coupling, so that the truncation identity later compares two independently
+described couplings. -/
+noncomputable def bipartiteLaw :
+    Measure (RelStructure digraphSig (Vinfinite digraphSig)) :=
+  (iidUniformSource (RankSupport digraphSig 1)).map arr
+
+instance : IsProbabilityMeasure bipartiteLaw :=
+  Measure.isProbabilityMeasure_map measurable_arr.aemeasurable
+
+theorem bipartiteLaw_map_relabel (σ : ∀ _ : Unit, Equiv.Perm ℕ) :
+    bipartiteLaw.map (RelStructure.relabel σ) = bipartiteLaw := by
+  rw [bipartiteLaw, Measure.map_map (measurable_relabel σ) measurable_arr,
+    show RelStructure.relabel σ ∘ arr =
+      arr ∘ (fun ω : Colours => fun A => ω (supportPerm (σ ()) A)) from by
+        funext ω
+        exact (arr_comp_supportPerm (σ ()) ω).symm,
+    ← Measure.map_map measurable_arr
+      (measurable_pi_lambda _ fun _ => measurable_pi_apply _),
+    iidUniformSource,
+    Measure.infinitePi_map_comp_equiv _ (supportPerm (σ ()))]
+
+/-- The bipartite law as an exchangeable law on the infinite structure space. -/
+noncomputable def bipartiteExchangeable : InfiniteRelExchangeableLaw digraphSig where
+  law := ⟨bipartiteLaw, inferInstance⟩
+  exchangeable := bipartiteLaw_map_relabel
+
+/-! ### Blocks of this signature
+
+For `digraphSig` every coordinate has a two-element or one-element support, never the empty one,
+and a singleton support forces the diagonal coordinate. -/
+
+instance : IsEmpty (BlockIndex (S := digraphSig) (∅ : Finset (Σ _ : Unit, ℕ))) :=
+  ⟨fun c => by
+    have hne := RelCoord.support_nonempty c.1 (by norm_num)
+    rw [c.2] at hne
+    exact absurd hne (by simp)⟩
+
+instance : Unique (BlockSpace (S := digraphSig) (∅ : Finset (Σ _ : Unit, ℕ))) :=
+  Pi.uniqueOfIsEmpty _
+
+open scoped Classical in
+/-- A coordinate whose support is the singleton `{v}` is the diagonal coordinate at `v`. -/
+theorem eq_digraphCoord_of_support_singleton {v : ℕ}
+    (c : BlockIndex (S := digraphSig) ({⟨(), v⟩} : Finset (Σ _ : Unit, ℕ))) :
+    c.1 = digraphCoord v v := by
+  have h0 : c.1.taggedValue 0 ∈ c.1.support := (RelCoord.mem_support_iff _ _).mpr ⟨0, rfl⟩
+  have h1 : c.1.taggedValue 1 ∈ c.1.support := (RelCoord.mem_support_iff _ _).mpr ⟨1, rfl⟩
+  rw [c.2, Finset.mem_singleton] at h0 h1
+  have e0 : c.1.2 0 = v := congrArg Sigma.snd h0
+  have e1 : c.1.2 1 = v := congrArg Sigma.snd h1
+  refine congrArg (fun w' => (⟨c.1.1, w'⟩ : RelCoord digraphSig (Vinfinite digraphSig))) ?_
+  funext i
+  fin_cases i
+  · exact e0
+  · exact e1
+
+open scoped Classical in
+/-- **The singleton block of this law is constantly `false`** — it reads only the diagonal. -/
+theorem blockMap_singleton_arr (ω : Colours) (v : ℕ) :
+    blockMap ({⟨(), v⟩} : Finset (Σ _ : Unit, ℕ)) (arr ω) = fun _ => false := by
+  funext c
+  show arr ω c.1 = false
+  rw [eq_digraphCoord_of_support_singleton c, arr_diagonal]
+
+/-! ### The rank-one coupling, defined independently of the rank-two one -/
+
+/-- **The rank-one coupling**: the bipartite law together with an *independent* global uniform
+`U_∅`. At rank one the latent cube is exactly that one coordinate — it is not trivial, and this
+coupling is described without reference to the rank-two object. -/
+noncomputable def rankOneCoupling :
+    Measure (RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 1) :=
+  bipartiteLaw.prod (rankLatentSource digraphSig 1)
+
+instance : IsProbabilityMeasure rankOneCoupling := by
+  rw [rankOneCoupling]; infer_instance
+
+@[simp] theorem rankOneCoupling_map_fst : rankOneCoupling.map Prod.fst = bipartiteLaw := by
+  rw [rankOneCoupling, Measure.map_fst_prod]
+  simp
+
+@[simp] theorem rankOneCoupling_map_snd :
+    rankOneCoupling.map Prod.snd = rankLatentSource digraphSig 1 := by
+  rw [rankOneCoupling, Measure.map_snd_prod]
+  simp
+
+open scoped Classical in
+/-- The singleton block is a.e. constant under the bipartite law. -/
+theorem ae_blockMap_singleton (v : ℕ) :
+    ∀ᵐ X ∂bipartiteLaw, blockMap ({⟨(), v⟩} : Finset (Σ _ : Unit, ℕ)) X = fun _ => false := by
+  rw [bipartiteLaw]
+  refine (ae_map_iff measurable_arr.aemeasurable ?_).mpr ?_
+  · exact (measurable_blockMap (S := digraphSig)
+      ({⟨(), v⟩} : Finset (Σ _ : Unit, ℕ)))
+      (measurableSet_singleton (x := (fun _ => false :
+        BlockSpace (S := digraphSig) ({⟨(), v⟩} : Finset (Σ _ : Unit, ℕ)))))
+  · exact Filter.Eventually.of_forall fun ω => blockMap_singleton_arr ω v
+
+open scoped Classical in
+/-- **The rank-one representation**, built directly from the independently described coupling. -/
+noncomputable def rankOneRep : bipartiteExchangeable.RankRepresentation 1 where
+  P := rankOneCoupling
+  isProbabilityMeasure_P := inferInstance
+  map_fst := rankOneCoupling_map_fst
+  map_snd := rankOneCoupling_map_snd
+  invariant := by
+    intro σ
+    have hfun : (Prod.map (RelStructure.relabel σ.1) (⇑(rankLatentRelabel σ 1)) :
+        RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 1 → _) =
+        Prod.map (RelStructure.relabel σ.1) id := by
+      funext p
+      exact Prod.ext rfl (rankLatentRelabel_one_eq σ p.2)
+    rw [rankOneCoupling, hfun,
+      ← Measure.map_prod_map _ _ (measurable_relabel σ.1) measurable_id,
+      bipartiteLaw_map_relabel, Measure.map_id]
+  lower_recovers := by
+    intro A hA
+    have hA0 : A = ∅ := Finset.card_eq_zero.mp (Nat.lt_one_iff.mp hA)
+    subst hA0
+    exact ⟨fun _ => default, measurable_const,
+      Filter.Eventually.of_forall fun _ => Subsingleton.elim _ _⟩
+  screening := by
+    intro A hA
+    obtain ⟨a, rfl⟩ := Finset.card_eq_one.mp hA
+    obtain ⟨u, v⟩ := a
+    cases u
+    have hae : blockMap ({⟨(), v⟩} : Finset (Σ _ : Unit, ℕ)) ∘ Prod.fst
+        =ᵐ[rankOneCoupling] fun _ => (fun _ => false) := by
+      have h := (Measure.quasiMeasurePreserving_fst (μ := bipartiteLaw)
+        (ν := rankLatentSource digraphSig 1)).ae (ae_blockMap_singleton v)
+      rw [rankOneCoupling]
+      exact h
+    exact CondIndepFun.congr
+      (condIndepFun_const_left (fun _ => false) _)
+      measurable_const (measurable_restObservation 1 _)
+      ((measurable_blockMap (S := digraphSig) _).comp measurable_fst)
+      (measurable_restObservation 1 _) hae.symm Filter.EventuallyEq.rfl
+
+end BipartiteRegression
+
+end RelSignature

From 6368ae4d63dea4924106c828e76d43d8a226ee58 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 17 Aug 2026 12:32:42 +0000
Subject: [PATCH 02/11] wip(#196): rank-two coupling and the three central
 identities
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Proved immediately after the definition, before invariance or screening
add noise, as directed:

1. rankTwoCoupling_map_fst = bipartiteLaw
2. rankTwoCoupling_map_snd = rankLatentSource 2
3. rankTwoCoupling_truncation = rankOneCoupling — the gate

The third visibly consumes rankLatentSource_map_rankLatentSpaceSuccEquiv:
U_∅ splits off from the singleton layer, the array reads only the
latter, the truncation reads only the former, and Measure.prod_swap plus
map_prod_map reassemble the independently defined product. It passed with
only orientation fixes, which is exactly what proving it early was meant
to surface.
---
 Graphon/RelBipartiteRegression.lean | 73 +++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)

diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index ebcfde1..c443c4b 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -272,6 +272,79 @@ noncomputable def rankOneRep : bipartiteExchangeable.RankRepresentation 1 where
       ((measurable_blockMap (S := digraphSig) _).comp measurable_fst)
       (measurable_restObservation 1 _) hae.symm Filter.EventuallyEq.rfl
 
+/-! ### The rank-two coupling and the three central identities
+
+The identities are proved immediately after the definition, before invariance or screening add
+noise. The third is the real gate: it visibly consumes the source factorization. -/
+
+/-- The fresh singleton layer of a rank-two latent point. -/
+noncomputable def freshLayer (ω : RankLatentSpace digraphSig 2) : Colours :=
+  (rankLatentSpaceSuccEquiv 1 ω).2
+
+theorem measurable_freshLayer : Measurable freshLayer :=
+  (rankLatentSpaceSuccEquiv 1).measurable.snd
+
+/-- **The rank-two coupling**: the array is built from the fresh singleton layer, and the whole
+rank-two latent point is retained. -/
+noncomputable def rankTwoCoupling :
+    Measure (RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 2) :=
+  (rankLatentSource digraphSig 2).map fun ω => (arr (freshLayer ω), ω)
+
+theorem measurable_rankTwoMap :
+    Measurable fun ω : RankLatentSpace digraphSig 2 => (arr (freshLayer ω), ω) :=
+  (measurable_arr.comp measurable_freshLayer).prodMk measurable_id
+
+instance : IsProbabilityMeasure rankTwoCoupling := by
+  rw [rankTwoCoupling]
+  exact Measure.isProbabilityMeasure_map measurable_rankTwoMap.aemeasurable
+
+/-- The fresh layer carries the i.i.d. singleton source — the second factor of the successor
+split. -/
+theorem map_freshLayer :
+    (rankLatentSource digraphSig 2).map freshLayer =
+      iidUniformSource (RankSupport digraphSig 1) := by
+  have hfl : freshLayer = Prod.snd ∘ (rankLatentSpaceSuccEquiv 1) := rfl
+  rw [hfl, ← Measure.map_map measurable_snd (rankLatentSpaceSuccEquiv 1).measurable,
+    rankLatentSource_map_rankLatentSpaceSuccEquiv, Measure.map_snd_prod]
+  simp
+
+/-- **Identity 1**: the structure marginal is the bipartite law. -/
+@[simp] theorem rankTwoCoupling_map_fst : rankTwoCoupling.map Prod.fst = bipartiteLaw := by
+  rw [rankTwoCoupling, Measure.map_map measurable_fst measurable_rankTwoMap,
+    show (Prod.fst ∘ fun ω : RankLatentSpace digraphSig 2 => (arr (freshLayer ω), ω)) =
+      arr ∘ freshLayer from rfl,
+    ← Measure.map_map measurable_arr measurable_freshLayer, map_freshLayer, bipartiteLaw]
+
+/-- **Identity 2**: the latent marginal is the rank-two source. -/
+@[simp] theorem rankTwoCoupling_map_snd :
+    rankTwoCoupling.map Prod.snd = rankLatentSource digraphSig 2 := by
+  rw [rankTwoCoupling, Measure.map_map measurable_snd measurable_rankTwoMap,
+    show (Prod.snd ∘ fun ω : RankLatentSpace digraphSig 2 => (arr (freshLayer ω), ω)) = id from rfl,
+    Measure.map_id]
+
+/-- **Identity 3 — the gate**: truncating the rank-two coupling's latents to rank one returns the
+*independently defined* rank-one coupling. This is where the source factorization is consumed:
+`U_∅` splits off from the singleton layer, the array depends only on the latter, and the
+truncation reads only the former. -/
+theorem rankTwoCoupling_truncation :
+    rankTwoCoupling.map (Prod.map id (rankLatentProjection (S := digraphSig) (Nat.le_succ 1))) =
+      rankOneCoupling := by
+  rw [rankTwoCoupling,
+    Measure.map_map (measurable_id.prodMap
+        (measurable_rankLatentProjection (S := digraphSig) (Nat.le_succ 1)))
+      measurable_rankTwoMap,
+    show (Prod.map (id : RelStructure digraphSig (Vinfinite digraphSig) → _)
+        (rankLatentProjection (S := digraphSig) (Nat.le_succ 1)) ∘
+        fun ω : RankLatentSpace digraphSig 2 => (arr (freshLayer ω), ω)) =
+      (Prod.map arr (id : RankLatentSpace digraphSig 1 → _)) ∘ Prod.swap ∘
+        (rankLatentSpaceSuccEquiv 1) from rfl,
+    ← Measure.map_map (measurable_arr.prodMap measurable_id)
+      (measurable_swap.comp (rankLatentSpaceSuccEquiv 1).measurable),
+    ← Measure.map_map measurable_swap (rankLatentSpaceSuccEquiv 1).measurable,
+    rankLatentSource_map_rankLatentSpaceSuccEquiv, Measure.prod_swap,
+    ← Measure.map_prod_map _ _ measurable_arr measurable_id, Measure.map_id,
+    rankOneCoupling, bipartiteLaw]
+
 end BipartiteRegression
 
 end RelSignature

From 5b12baa0380177751a959a4631f93aedfd1c2623 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 17 Aug 2026 20:41:18 +0000
Subject: [PATCH 03/11] wip(#196): recovery below rank two, from the pieces
 already established
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

lower_recovers at rank two ranges over supports of cardinality < 2, so
it sees only the empty and singleton cases and never a two-point
support — the two-point decoder plays no part. The empty case is vacuous
for this signature (no coordinate has empty support), the singleton case
is the constantly-false diagonal, transported through identity 1
(rankTwoCoupling_map_fst) as a measure-preserving projection.

Statement pins (S := digraphSig) on LocalLatentSpace/BlockSpace/
localLatents: with A : Finset (Σ _ : Unit, ℕ) the signature is otherwise
a metavariable.
---
 Graphon/RelBipartiteRegression.lean | 32 +++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index c443c4b..7eb0c67 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -345,6 +345,38 @@ theorem rankTwoCoupling_truncation :
     ← Measure.map_prod_map _ _ measurable_arr measurable_id, Measure.map_id,
     rankOneCoupling, bipartiteLaw]
 
+/-! ### Recovery below rank two
+
+`lower_recovers` at rank two ranges over supports of cardinality `< 2`, so it sees only the empty
+and singleton cases — never a two-point support. Both blocks are deterministic: the empty one is
+vacuous for this signature, the singleton one is the constantly-false diagonal. The two-point
+decoder plays no part here. -/
+
+open scoped Classical in
+theorem lower_recovers_rank_two (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card < 2) :
+    ∃ g : LocalLatentSpace (S := digraphSig) A 2 → BlockSpace (S := digraphSig) A,
+      Measurable g ∧
+      (fun p : RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 2 =>
+          blockMap (S := digraphSig) A p.1) =ᵐ[rankTwoCoupling]
+        fun p => g (localLatents (S := digraphSig) A 2 p.2) := by
+  have hcase : A.card = 0 ∨ A.card = 1 := by omega
+  rcases hcase with h0 | h1
+  · -- the empty support: no coordinate of this signature has empty support
+    have hA0 : A = ∅ := Finset.card_eq_zero.mp h0
+    subst hA0
+    exact ⟨fun _ => default, measurable_const,
+      Filter.Eventually.of_forall fun _ => Subsingleton.elim _ _⟩
+  · -- a singleton support: the block is the constantly-false diagonal
+    obtain ⟨a, rfl⟩ := Finset.card_eq_one.mp h1
+    obtain ⟨u, v⟩ := a
+    cases u
+    refine ⟨fun _ => fun _ => false, measurable_const, ?_⟩
+    have hmp : MeasurePreserving (Prod.fst :
+        RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 2 → _)
+        rankTwoCoupling bipartiteLaw :=
+      ⟨measurable_fst, rankTwoCoupling_map_fst⟩
+    exact hmp.quasiMeasurePreserving.ae (ae_blockMap_singleton v)
+
 end BipartiteRegression
 
 end RelSignature

From 33231d609b584e73671b772d2b5f5fc141edac5e Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Mon, 17 Aug 2026 23:42:48 +0000
Subject: [PATCH 04/11] wip(#196): the two-point deterministic-block lemma
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

blockMap_pair_arr: on a two-point support the whole directed block is the
deterministic parity of the two singleton latents visible there. BOTH
X_uv and X_vu decode to the same value — symmetry exhibited as a property
of this law, not of the signature.

Supporting: pairSupport / pairLocalIndex / twoPointDecoder with its
measurability, coord_of_pair (a two-point block coordinate is one of the
two directed pairs, the degenerate diagonal cases ruled out by u ≠ v via
the two vertex witnesses), and freshLayer_vertexSupport, which is rfl —
the successor split's inverse keeps the same underlying finset, so the
decoder reads the fresh layer with no transport.

This lemma organizes rank-two screening and the public XOR identity, and
nothing else: lower_recovers at rank two ranges over cardinality < 2 and
keeps its own vacuous/constant-diagonal proof.
---
 Graphon/RelBipartiteRegression.lean | 101 ++++++++++++++++++++++++++++
 1 file changed, 101 insertions(+)

diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index 7eb0c67..d4d61c0 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -61,6 +61,20 @@ information, which is what makes its rank-one recovery and screening determinist
 @[simp] theorem arr_diagonal (ω : Colours) (v : ℕ) : arr ω (digraphCoord v v) = false := by
   simp [arr_apply, Bool.xor_self]
 
+/-- Thresholding a measurable real at `1/2` is measurable. -/
+theorem measurable_decideLe {X : Type*} [MeasurableSpace X] {f : X → ℝ} (hf : Measurable f) :
+    Measurable fun x => decide (f x ≤ 1 / 2) := by
+  refine measurable_to_countable' fun b => ?_
+  cases b
+  · have hpre : (fun x => decide (f x ≤ 1 / 2)) ⁻¹' {false} = {x | f x ≤ 1 / 2}ᶜ := by
+      ext x; simp
+    rw [hpre]
+    exact (measurableSet_le hf measurable_const).compl
+  · have hpre : (fun x => decide (f x ≤ 1 / 2)) ⁻¹' {true} = {x | f x ≤ 1 / 2} := by
+      ext x; simp
+    rw [hpre]
+    exact measurableSet_le hf measurable_const
+
 theorem measurable_colour (v : ℕ) : Measurable fun ω : Colours => colour ω v := by
   refine measurable_to_countable' fun b => ?_
   cases b
@@ -377,6 +391,93 @@ theorem lower_recovers_rank_two (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card < 2
       ⟨measurable_fst, rankTwoCoupling_map_fst⟩
     exact hmp.quasiMeasurePreserving.ae (ae_blockMap_singleton v)
 
+/-! ### The two-point deterministic block
+
+The organizing lemma for rank-two screening and for the public XOR identity: on a two-point
+support the whole directed block — *both* coordinates `X_uv` and `X_vu` — is a deterministic
+function of the two singleton latents visible there. Recovering both as the same parity is what
+exhibits symmetry as a property of this law rather than of the signature. -/
+
+/-- The two-point support at a pair of distinct vertices. -/
+def pairSupport (u v : ℕ) : Finset (Σ _ : Unit, ℕ) := {⟨(), u⟩, ⟨(), v⟩}
+
+@[simp] theorem mem_pairSupport_left (u v : ℕ) :
+    (⟨(), u⟩ : Σ _ : Unit, ℕ) ∈ pairSupport u v := by simp [pairSupport]
+
+@[simp] theorem mem_pairSupport_right (u v : ℕ) :
+    (⟨(), v⟩ : Σ _ : Unit, ℕ) ∈ pairSupport u v := by simp [pairSupport]
+
+open scoped Classical in
+/-- A vertex of the pair, as a latent index visible at that support. -/
+def pairLocalIndex (u v w : ℕ) (h : (⟨(), w⟩ : Σ _ : Unit, ℕ) ∈ pairSupport u v) :
+    LocalLatentIndex (S := digraphSig) (pairSupport u v) 2 :=
+  ⟨⟨{⟨(), w⟩}, by simp⟩, by simpa using h⟩
+
+open scoped Classical in
+/-- **The two-point decoder**: read the two singleton latents and return their parity, for every
+coordinate of the block. -/
+noncomputable def twoPointDecoder (u v : ℕ) :
+    LocalLatentSpace (S := digraphSig) (pairSupport u v) 2 →
+      BlockSpace (S := digraphSig) (pairSupport u v) := fun l _ =>
+  xor (decide (l (pairLocalIndex u v u (mem_pairSupport_left u v)) ≤ 1 / 2))
+    (decide (l (pairLocalIndex u v v (mem_pairSupport_right u v)) ≤ 1 / 2))
+
+theorem measurable_twoPointDecoder (u v : ℕ) : Measurable (twoPointDecoder u v) := by
+  refine measurable_pi_lambda _ fun _ => ?_
+  exact (Measurable.of_discrete (f := fun p : Bool × Bool => xor p.1 p.2)).comp
+    ((measurable_decideLe (measurable_pi_apply _)).prodMk
+      (measurable_decideLe (measurable_pi_apply _)))
+
+open scoped Classical in
+/-- A coordinate of a two-point block is one of the two directed pairs. -/
+theorem coord_of_pair {u v : ℕ} (huv : u ≠ v)
+    (c : BlockIndex (S := digraphSig) (pairSupport u v)) :
+    (c.1.2 0 = u ∧ c.1.2 1 = v) ∨ (c.1.2 0 = v ∧ c.1.2 1 = u) := by
+  have h0 : c.1.taggedValue 0 ∈ c.1.support := (RelCoord.mem_support_iff _ _).mpr ⟨0, rfl⟩
+  have h1 : c.1.taggedValue 1 ∈ c.1.support := (RelCoord.mem_support_iff _ _).mpr ⟨1, rfl⟩
+  have hu : (⟨(), u⟩ : Σ _ : Unit, ℕ) ∈ c.1.support := by rw [c.2]; simp
+  have hv : (⟨(), v⟩ : Σ _ : Unit, ℕ) ∈ c.1.support := by rw [c.2]; simp
+  rw [c.2] at h0 h1
+  rw [(RelCoord.mem_support_iff _ _)] at hu hv
+  obtain ⟨iu, hiu⟩ := hu
+  obtain ⟨iv, hiv⟩ := hv
+  simp only [RelCoord.taggedValue, pairSupport, Finset.mem_insert, Finset.mem_singleton,
+    Sigma.mk.injEq, heq_eq_eq, true_and] at h0 h1
+  simp only [RelCoord.taggedValue, Sigma.mk.injEq, heq_eq_eq, true_and] at hiu hiv
+  rcases h0 with h0 | h0 <;> rcases h1 with h1 | h1
+  · exfalso
+    fin_cases iv <;> simp_all
+  · exact Or.inl ⟨h0, h1⟩
+  · exact Or.inr ⟨h0, h1⟩
+  · exfalso
+    fin_cases iu <;> simp_all
+
+open scoped Classical in
+/-- The fresh layer at a vertex is the rank-two latent at that singleton support. -/
+theorem freshLayer_vertexSupport (ω : RankLatentSpace digraphSig 2) (w : ℕ) :
+    freshLayer ω (vertexSupport w) = ω ⟨{⟨(), w⟩}, by simp⟩ := rfl
+
+open scoped Classical in
+/-- **The organizing lemma**: on a two-point support the whole directed block is the deterministic
+parity of the two singleton latents visible there. Both `X_uv` and `X_vu` decode to the same
+value, so the symmetry of this law is exhibited rather than assumed. -/
+theorem blockMap_pair_arr {u v : ℕ} (huv : u ≠ v) (ω : RankLatentSpace digraphSig 2) :
+    blockMap (S := digraphSig) (pairSupport u v) (arr (freshLayer ω)) =
+      twoPointDecoder u v (localLatents (S := digraphSig) (pairSupport u v) 2 ω) := by
+  funext c
+  show arr (freshLayer ω) c.1 = _
+  have hdec : ∀ w : ℕ, colour (freshLayer ω) w = decide (ω ⟨{⟨(), w⟩}, by simp⟩ ≤ 1 / 2) := by
+    intro w
+    rw [colour, freshLayer_vertexSupport]
+  have hl : ∀ (w : ℕ) (h : (⟨(), w⟩ : Σ _ : Unit, ℕ) ∈ pairSupport u v),
+      localLatents (S := digraphSig) (pairSupport u v) 2 ω (pairLocalIndex u v w h)
+        = ω ⟨{⟨(), w⟩}, by simp⟩ := fun _ _ => rfl
+  show xor (colour (freshLayer ω) (c.1.2 0)) (colour (freshLayer ω) (c.1.2 1)) = _
+  rw [twoPointDecoder, hl u (mem_pairSupport_left u v), hl v (mem_pairSupport_right u v)]
+  rcases coord_of_pair huv c with ⟨e0, e1⟩ | ⟨e0, e1⟩
+  · rw [e0, e1, hdec, hdec]
+  · rw [e0, e1, hdec, hdec, Bool.xor_comm]
+
 end BipartiteRegression
 
 end RelSignature

From 924ab0ad182143d00b23b41164c41881e4825af9 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 18 Aug 2026 01:58:50 +0000
Subject: [PATCH 05/11] wip(#196): rank-two screening via the
 deterministic-block lemma
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

exists_pairSupport_of_card_two normalizes an arbitrary two-point support
to pairSupport u v with u ≠ v FIRST, via an obtain with rfl, so
blockMap_pair_arr applies directly and no dependent block or
local-latent space is transported across a later equality.

Screening is then exactly the three steps: push the source-level decoder
identity to an a.e. identity under rankTwoCoupling (ae_blockMap_pair, via
ae_map_iff and measurableSet_eq_fun), replace the block observation with
CondIndepFun.congr, and discharge conditional independence with
condIndepFun_of_measurable_left — the decoder is measurable through
localLatents, hence measurable for the conditioning sigma-algebra by
comap_measurable. No conditional-expectation reasoning appears.
---
 Graphon/RelBipartiteRegression.lean | 48 +++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index d4d61c0..6df9d66 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -478,6 +478,54 @@ theorem blockMap_pair_arr {u v : ℕ} (huv : u ≠ v) (ω : RankLatentSpace digr
   · rw [e0, e1, hdec, hdec]
   · rw [e0, e1, hdec, hdec, Bool.xor_comm]
 
+/-! ### Rank-two screening
+
+The arbitrary two-point support is normalized to `pairSupport u v` *first*, so that the
+deterministic-block lemma applies directly and no dependent block or local-latent space has to be
+transported across a later equality. -/
+
+open scoped Classical in
+/-- A support of cardinality two is a `pairSupport` at distinct vertices. -/
+theorem exists_pairSupport_of_card_two {A : Finset (Σ _ : Unit, ℕ)} (hA : A.card = 2) :
+    ∃ u v : ℕ, u ≠ v ∧ A = pairSupport u v := by
+  obtain ⟨a, b, hab, rfl⟩ := Finset.card_eq_two.mp hA
+  refine ⟨a.2, b.2, fun h => hab ?_, rfl⟩
+  exact Sigma.ext rfl (heq_of_eq h)
+
+open scoped Classical in
+/-- The decoder identity holds a.e. under the rank-two coupling. -/
+theorem ae_blockMap_pair {u v : ℕ} (huv : u ≠ v) :
+    (fun p : RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 2 =>
+        blockMap (S := digraphSig) (pairSupport u v) p.1) =ᵐ[rankTwoCoupling]
+      fun p => twoPointDecoder u v (localLatents (S := digraphSig) (pairSupport u v) 2 p.2) := by
+  rw [rankTwoCoupling]
+  refine (ae_map_iff measurable_rankTwoMap.aemeasurable ?_).mpr
+    (Filter.Eventually.of_forall fun ω => blockMap_pair_arr huv ω)
+  exact measurableSet_eq_fun
+    ((measurable_blockMap (S := digraphSig) _).comp measurable_fst)
+    ((measurable_twoPointDecoder u v).comp
+      ((measurable_localLatents (S := digraphSig) _ 2).comp measurable_snd))
+
+open scoped Classical in
+/-- **Rank-two screening**: at a two-point support the block is conditionally independent of the
+rank-truncated remainder given the latents visible there — because it *is* a measurable function
+of them. -/
+theorem screening_rank_two (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card = 2) :
+    CondIndepFun (MeasurableSpace.comap
+        (localLatents (S := digraphSig) A 2 ∘ Prod.snd) inferInstance)
+      (((measurable_localLatents (S := digraphSig) A 2).comp measurable_snd).comap_le)
+      (blockMap (S := digraphSig) A ∘ Prod.fst) (restObservation 2 A) rankTwoCoupling := by
+  obtain ⟨u, v, huv, rfl⟩ := exists_pairSupport_of_card_two hA
+  refine CondIndepFun.congr
+    (condIndepFun_of_measurable_left
+      ((measurable_twoPointDecoder u v).comp (comap_measurable _))
+      (measurable_restObservation 2 _))
+    ((measurable_twoPointDecoder u v).comp
+      ((measurable_localLatents (S := digraphSig) _ 2).comp measurable_snd))
+    (measurable_restObservation 2 _)
+    ((measurable_blockMap (S := digraphSig) _).comp measurable_fst)
+    (measurable_restObservation 2 _) (ae_blockMap_pair huv).symm Filter.EventuallyEq.rfl
+
 end BipartiteRegression
 
 end RelSignature

From 9006cca4b2a1dc9a4c3444a6d268a4cae5784b1c Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 18 Aug 2026 02:17:08 +0000
Subject: [PATCH 06/11] feat(#196): the bipartite successor witness
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

rankTwoRep assembles all seven fields from the theorems above, and

  bipartiteSuccessor : RankSuccessor rankOneRep

is a two-field literal whose truncation proof is exactly
rankTwoCoupling_truncation. The successor contract is now satisfied by an
explicit rank 1 -> 2 example whose two couplings were described
INDEPENDENTLY — the array law from the fresh singleton layer, the
rank-one coupling as a product with U_∅ — so the truncation identity is a
theorem about two separate descriptions rather than bookkeeping.

Invariance came from one exact pointwise joint-action lemma proved before
any measure was touched, isolating the orientation conventions; the
rankSupportEquiv/supportPerm bridge is kept local, since the finitely
supported rank action and the full-permutation helper serve different
APIs.
---
 Graphon/RelBipartiteRegression.lean | 78 +++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)

diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index 6df9d66..af740e0 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -526,6 +526,84 @@ theorem screening_rank_two (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card = 2) :
     ((measurable_blockMap (S := digraphSig) _).comp measurable_fst)
     (measurable_restObservation 2 _) (ae_blockMap_pair huv).symm Filter.EventuallyEq.rfl
 
+/-! ### The joint action
+
+One exact pointwise lemma, proved before any measure is touched, so that the inverse and
+orientation conventions are isolated in a single place. -/
+
+open scoped Classical in
+/-- The finitely supported rank-support action agrees with the full-permutation helper. Kept local
+to this file: the two serve genuinely different APIs. -/
+theorem rankSupportEquiv_eq_supportPerm (σ : FinSuppPerm digraphSig)
+    (A : RankSupport digraphSig 1) : rankSupportEquiv σ 1 A = supportPerm (σ.1 ()) A := by
+  refine Subtype.ext ?_
+  refine Finset.ext fun w => ?_
+  simp only [rankSupportEquiv, supportPerm, Equiv.coe_fn_mk, Finset.mem_image]
+
+open scoped Classical in
+/-- The fresh layer intertwines the rank-two latent action with the vertex action. -/
+theorem freshLayer_rankLatentRelabel (σ : FinSuppPerm digraphSig)
+    (ω : RankLatentSpace digraphSig 2) :
+    freshLayer (rankLatentRelabel σ 2 ω) = fun A => freshLayer ω (supportPerm (σ.1 ()) A) := by
+  funext A
+  show (rankLatentSpaceSuccEquiv 1 (rankLatentRelabel σ 2 ω)).2 A = _
+  rw [show rankLatentSpaceSuccEquiv 1 (rankLatentRelabel σ 2 ω) =
+      MeasurableEquiv.prodCongr (rankLatentRelabel σ 1) (rankSupportLatentRelabel σ 1)
+        (rankLatentSpaceSuccEquiv 1 ω) from
+    congrFun (rankLatentSpaceSuccEquiv_rankLatentRelabel σ 1) ω]
+  show freshLayer ω (rankSupportEquiv σ 1 A) = _
+  rw [rankSupportEquiv_eq_supportPerm]
+
+open scoped Classical in
+/-- **The exact pointwise joint action.** Relabeling the rank-two latent point and then building
+the pair is the same as building the pair and acting diagonally. -/
+theorem jointMap_rankLatentRelabel (σ : FinSuppPerm digraphSig)
+    (ω : RankLatentSpace digraphSig 2) :
+    (arr (freshLayer (rankLatentRelabel σ 2 ω)), rankLatentRelabel σ 2 ω) =
+      Prod.map (RelStructure.relabel σ.1) (⇑(rankLatentRelabel σ 2))
+        (arr (freshLayer ω), ω) := by
+  refine Prod.ext ?_ rfl
+  show arr (freshLayer (rankLatentRelabel σ 2 ω)) = RelStructure.relabel σ.1 (arr (freshLayer ω))
+  rw [freshLayer_rankLatentRelabel, arr_comp_supportPerm]
+
+/-- **Rank-two invariance**, now just `Measure.map_map`, the joint action, and source
+invariance. -/
+theorem rankTwoCoupling_invariant (σ : FinSuppPerm digraphSig) :
+    rankTwoCoupling.map (Prod.map (RelStructure.relabel σ.1) (⇑(rankLatentRelabel σ 2))) =
+      rankTwoCoupling := by
+  rw [rankTwoCoupling,
+    Measure.map_map ((measurable_relabel σ.1).prodMap (rankLatentRelabel σ 2).measurable)
+      measurable_rankTwoMap,
+    show (Prod.map (RelStructure.relabel σ.1) (⇑(rankLatentRelabel σ 2)) ∘
+        fun ω : RankLatentSpace digraphSig 2 => (arr (freshLayer ω), ω)) =
+      (fun ω : RankLatentSpace digraphSig 2 => (arr (freshLayer ω), ω)) ∘
+        (⇑(rankLatentRelabel σ 2)) from by
+      funext ω
+      exact (jointMap_rankLatentRelabel σ ω).symm,
+    ← Measure.map_map measurable_rankTwoMap (rankLatentRelabel σ 2).measurable,
+    rankLatentSource_map_rankLatentRelabel]
+
+/-! ### The representation and the successor witness -/
+
+open scoped Classical in
+/-- **The rank-two representation.** Every field is one of the theorems above. -/
+noncomputable def rankTwoRep : bipartiteExchangeable.RankRepresentation 2 where
+  P := rankTwoCoupling
+  isProbabilityMeasure_P := inferInstance
+  map_fst := rankTwoCoupling_map_fst
+  map_snd := rankTwoCoupling_map_snd
+  invariant := rankTwoCoupling_invariant
+  lower_recovers := lower_recovers_rank_two
+  screening := screening_rank_two
+
+/-- **The successor witness**: a two-field literal whose truncation proof is exactly the gate
+identity. This is the regression's headline — the contract is satisfied by an explicit rank
+`1 → 2` example whose two couplings were described independently. -/
+noncomputable def bipartiteSuccessor :
+    InfiniteRelExchangeableLaw.RankSuccessor rankOneRep where
+  next := rankTwoRep
+  truncation := rankTwoCoupling_truncation
+
 end BipartiteRegression
 
 end RelSignature

From 90e7c01e3a72e423eeebfd5d7869c6d3e29e2a53 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 18 Aug 2026 02:17:59 +0000
Subject: [PATCH 07/11] feat(#196): the public XOR identity, projected from the
 block lemma
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

ae_edge_xor: almost surely the edge at a pair of distinct vertices is the
parity of their two colours. Obtained by evaluating the deterministic-block
identity at one coordinate — no second pushforward calculation, as
intended. support_digraphCoord records that the directed coordinate lies
in that pair's block.
---
 Graphon/RelBipartiteRegression.lean | 35 +++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index af740e0..1cc91a9 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -604,6 +604,41 @@ noncomputable def bipartiteSuccessor :
   next := rankTwoRep
   truncation := rankTwoCoupling_truncation
 
+/-! ### The public XOR identity
+
+A coordinate projection of the deterministic-block lemma — no second pushforward calculation. -/
+
+open scoped Classical in
+/-- The directed coordinate at a pair of distinct vertices lies in that pair's block. -/
+theorem support_digraphCoord {u v : ℕ} :
+    (digraphCoord u v : RelCoord digraphSig (Vinfinite digraphSig)).support = pairSupport u v := by
+  refine Finset.ext fun w => ?_
+  rw [RelCoord.mem_support_iff]
+  simp only [pairSupport, 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⟩
+
+open scoped Classical in
+/-- **The XOR identity**: almost surely the edge at a pair of distinct vertices is the parity of
+their two colours. Obtained by evaluating the block identity at one coordinate. -/
+theorem ae_edge_xor {u v : ℕ} (huv : u ≠ v) :
+    ∀ᵐ p ∂rankTwoCoupling, p.1 (digraphCoord u v) =
+      xor (colour (freshLayer p.2) u) (colour (freshLayer p.2) v) := by
+  filter_upwards [ae_blockMap_pair huv] with p hp
+  have := congrFun hp ⟨digraphCoord u v, support_digraphCoord⟩
+  rw [twoPointDecoder] at this
+  rw [show p.1 (digraphCoord u v) =
+      blockMap (S := digraphSig) (pairSupport u v) p.1
+        ⟨digraphCoord u v, support_digraphCoord⟩ from rfl, this]
+  rw [colour, colour, freshLayer_vertexSupport, freshLayer_vertexSupport]
+  rfl
+
 end BipartiteRegression
 
 end RelSignature

From d9ad730d93c0a589aa4756c972354bce0f84d020 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 18 Aug 2026 02:33:16 +0000
Subject: [PATCH 08/11] refactor: relocate uniform01_Iic to SamplerSources
 (#196)

It is a general fact about uniform01, which is defined in
SamplerSources, but it lived in the graph-specific InfiniteSampler. The
bipartite regression needs it and must not import that module for it.
Both existing consumers (InfiniteSampler, SampleExposure) compile
unchanged, since they already import SamplerSources.
---
 Graphon/InfiniteSampler.lean        | 10 ----------
 Graphon/RelBipartiteRegression.lean |  2 +-
 Graphon/SamplerSources.lean         | 10 ++++++++++
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/Graphon/InfiniteSampler.lean b/Graphon/InfiniteSampler.lean
index 4e1c8bf..25c5e11 100644
--- a/Graphon/InfiniteSampler.lean
+++ b/Graphon/InfiniteSampler.lean
@@ -142,16 +142,6 @@ probability is the clamped edge product; integrating out the positions gives
 
 section Marginal
 
-/-- The lower-interval mass of the uniform distribution on `[0,1]`. -/
-theorem uniform01_Iic {c : ℝ} (hc : c ∈ Set.Icc (0 : ℝ) 1) :
-    uniform01 (Set.Iic c) = ENNReal.ofReal c := by
-  rw [uniform01, Measure.restrict_apply measurableSet_Iic]
-  have h : Set.Iic c ∩ Set.Icc 0 1 = Set.Icc 0 c := by
-    ext x
-    simp only [Set.mem_inter_iff, Set.mem_Iic, Set.mem_Icc]
-    exact ⟨fun h => ⟨h.2.1, h.1⟩, fun h => ⟨h.2, h.1, h.2.trans hc.2⟩⟩
-  rw [h, Real.volume_Icc, sub_zero]
-
 /-- The joint law of the first `k` vertex positions is the finite i.i.d. product. -/
 theorem vertexSource_map_fin [IsProbabilityMeasure μ] (k : ℕ) :
     (vertexSource μ).map (fun (x : ℕ → α) (a : Fin k) => x ↑a) =
diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index 1cc91a9..c66c37d 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -59,7 +59,7 @@ noncomputable def arr (ω : Colours) : RelStructure digraphSig (Vinfinite digrap
 /-- **The diagonal is constantly false** — the singleton-support block of this law carries no
 information, which is what makes its rank-one recovery and screening deterministic. -/
 @[simp] theorem arr_diagonal (ω : Colours) (v : ℕ) : arr ω (digraphCoord v v) = false := by
-  simp [arr_apply, Bool.xor_self]
+  simp [arr_apply]
 
 /-- Thresholding a measurable real at `1/2` is measurable. -/
 theorem measurable_decideLe {X : Type*} [MeasurableSpace X] {f : X → ℝ} (hf : Measurable f) :
diff --git a/Graphon/SamplerSources.lean b/Graphon/SamplerSources.lean
index 14ee14a..6d52d76 100644
--- a/Graphon/SamplerSources.lean
+++ b/Graphon/SamplerSources.lean
@@ -69,6 +69,16 @@ instance : IsProbabilityMeasure uniform01 :=
   ⟨by rw [uniform01, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter,
     Real.volume_Icc]; norm_num⟩
 
+/-- The lower-interval mass of the uniform distribution on `[0,1]`. -/
+theorem uniform01_Iic {c : ℝ} (hc : c ∈ Set.Icc (0 : ℝ) 1) :
+    uniform01 (Set.Iic c) = ENNReal.ofReal c := by
+  rw [uniform01, Measure.restrict_apply measurableSet_Iic]
+  have h : Set.Iic c ∩ Set.Icc 0 1 = Set.Icc 0 c := by
+    ext x
+    simp only [Set.mem_inter_iff, Set.mem_Iic, Set.mem_Icc]
+    exact ⟨fun h => ⟨h.2.1, h.1⟩, fun h => ⟨h.2, h.1, h.2.trans hc.2⟩⟩
+  rw [h, Real.volume_Icc, sub_zero]
+
 /-- **The vertex source**: i.i.d. positions `ℕ → α` with law `μ`. -/
 noncomputable def iidVertexSource {α : Type*} [MeasurableSpace α] (μ : Measure α) :
     Measure (ℕ → α) :=

From bd75788342c0e43a47695df8204bd30e57c6dd93 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 18 Aug 2026 03:14:20 +0000
Subject: [PATCH 09/11] feat(#196): the XOR event has mass one half
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Via the repository-native route: Measure.infinitePi_map_comp_of_injective
at delta := Fin 2 with f := ![vertexSupport 0, vertexSupport 1] gives the
two-vertex marginal as Measure.pi (fun _ : Fin 2 => uniform01); the
XOR-true event is the disjoint union of the two rectangles Iic(1/2) x
Iic(1/2)ᶜ and its mirror, each of mass 1/4 by Measure.pi_pi with
uniform01_Iic_half and its complement.

This is the arithmetic that rules out the degenerate reading: a constant
edge would also be 'a function of the colours', but could not have this
mass.
---
 Graphon/RelBipartiteRegression.lean | 71 +++++++++++++++++++++++++++++
 1 file changed, 71 insertions(+)

diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index c66c37d..0777b89 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -33,6 +33,7 @@ the parity `colour u ⊕ colour v`.
 -/
 
 open MeasureTheory ProbabilityTheory
+open scoped ENNReal
 
 namespace RelSignature
 
@@ -639,6 +640,76 @@ theorem ae_edge_xor {u v : ℕ} (huv : u ≠ v) :
   rw [colour, colour, freshLayer_vertexSupport, freshLayer_vertexSupport]
   rfl
 
+/-! ### The numerical nonindependence witness
+
+"The edge is a function of the colours" would also hold for a constant edge. What rules that out
+is arithmetic: the edge event and the matching colour-parity event each have probability `1/2`,
+they coincide, and so their joint probability is `1/2` against a product of marginals `1/4`. -/
+
+/-- The two vertices `0` and `1`, as fresh-layer indices. -/
+def pairIndex : Fin 2 → RankSupport digraphSig 1 := ![vertexSupport 0, vertexSupport 1]
+
+theorem vertexSupport_injective : Function.Injective vertexSupport := by
+  intro a b h
+  have := congrArg Subtype.val h
+  simpa [vertexSupport] using this
+
+theorem pairIndex_injective : Function.Injective pairIndex := by
+  intro a b h
+  fin_cases a <;> fin_cases b <;>
+    simp_all [pairIndex, vertexSupport_injective.eq_iff]
+
+/-- **The two-vertex marginal** of the fresh source is the two-fold uniform product. -/
+theorem source_map_pairIndex :
+    (iidUniformSource (RankSupport digraphSig 1)).map (fun x d => x (pairIndex d)) =
+      Measure.pi fun _ : Fin 2 => uniform01 := by
+  rw [iidUniformSource]
+  exact Measure.infinitePi_map_comp_of_injective _ pairIndex_injective
+
+theorem uniform01_Iic_half : uniform01 (Set.Iic (1 / 2 : ℝ)) = 1 / 2 := by
+  rw [uniform01_Iic (by norm_num)]
+  rw [show (1 / 2 : ℝ) = ((1 : ℝ) / 2) from rfl]
+  rw [ENNReal.ofReal_div_of_pos (by norm_num), ENNReal.ofReal_one, ENNReal.ofReal_ofNat]
+
+theorem uniform01_Iic_half_compl : uniform01 (Set.Iic (1 / 2 : ℝ))ᶜ = 1 / 2 := by
+  have h := measure_compl (μ := uniform01) (s := Set.Iic (1 / 2 : ℝ)) measurableSet_Iic
+    (measure_ne_top _ _)
+  rw [h, measure_univ, uniform01_Iic_half]
+  rw [ENNReal.sub_eq_of_eq_add (by norm_num)]
+  norm_num
+  exact ENNReal.inv_two_add_inv_two.symm
+
+open scoped Classical in
+/-- **The XOR event has mass one half** on the two-vertex marginal: it is the disjoint union of
+two rectangles, each of mass `1/4`. -/
+theorem measure_xorTrue :
+    (Measure.pi fun _ : Fin 2 => uniform01)
+        {y : Fin 2 → ℝ | xor (decide (y 0 ≤ 1 / 2)) (decide (y 1 ≤ 1 / 2)) = true} = 1 / 2 := by
+  have hset : {y : Fin 2 → ℝ | xor (decide (y 0 ≤ 1 / 2)) (decide (y 1 ≤ 1 / 2)) = true} =
+      (Set.univ.pi ![Set.Iic (1 / 2 : ℝ), (Set.Iic (1 / 2 : ℝ))ᶜ]) ∪
+        (Set.univ.pi ![(Set.Iic (1 / 2 : ℝ))ᶜ, Set.Iic (1 / 2 : ℝ)]) := by
+    ext y
+    simp only [Set.mem_setOf_eq, Set.mem_union, Set.mem_univ_pi, Fin.forall_fin_two,
+      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Set.mem_Iic,
+      Set.mem_compl_iff]
+    by_cases h0 : y 0 ≤ 1 / 2 <;> by_cases h1 : y 1 ≤ 1 / 2 <;>
+      simp only [one_div] at h0 h1 <;> simp [h0, h1, not_le.mp]
+  have hdisj : Disjoint (Set.univ.pi ![Set.Iic (1 / 2 : ℝ), (Set.Iic (1 / 2 : ℝ))ᶜ])
+      (Set.univ.pi ![(Set.Iic (1 / 2 : ℝ))ᶜ, Set.Iic (1 / 2 : ℝ)]) := by
+    refine Set.disjoint_left.mpr fun y hy hy' => ?_
+    simp only [Set.mem_univ_pi, Fin.forall_fin_two, Matrix.cons_val_zero, Matrix.cons_val_one,
+      Matrix.head_cons, Set.mem_Iic, Set.mem_compl_iff] at hy hy'
+    exact hy'.1 hy.1
+  have hmeas : MeasurableSet (Set.univ.pi ![(Set.Iic (1 / 2 : ℝ))ᶜ, Set.Iic (1 / 2 : ℝ)]) := by
+    refine MeasurableSet.univ_pi fun i => ?_
+    fin_cases i
+    · exact measurableSet_Iic.compl
+    · exact measurableSet_Iic
+  rw [hset, measure_union hdisj hmeas, Measure.pi_pi, Measure.pi_pi]
+  simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
+    Fin.prod_univ_two, uniform01_Iic_half, uniform01_Iic_half_compl]
+  rw [← add_mul, ENNReal.add_halves, one_mul]
+
 end BipartiteRegression
 
 end RelSignature

From 428966b9cfd8bf38e84d3542aaab74d1e2c38c39 Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 18 Aug 2026 03:41:26 +0000
Subject: [PATCH 10/11] =?UTF-8?q?feat(#196):=20complete=20the=20bipartite?=
 =?UTF-8?q?=20regression=20=E2=80=94=20numerical=20nonindependence?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

not_indepFun_rankTwoCoupling: the array is NOT independent of its new
latent layer. The edge and colour-parity events coincide a.e., each has
probability 1/2, so their joint is 1/2 against a product of marginals
1/4. A constant edge would also be 'a function of the colours' but could
not achieve this, which is why the witness is numerical rather than
functional.

All null-set reasoning is confined to one a.e. event-equivalence lemma
(ae_edgeEvent_iff_parityEvent); the final theorem is pure arithmetic.

Wired into Graphon.lean with a doc bullet; audit 409 -> 415.
---
 Graphon.lean                        |  2 +
 Graphon/RelBipartiteRegression.lean | 91 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean            |  8 +++
 scripts/check_census_and_axioms.py  |  6 ++
 4 files changed, 107 insertions(+)

diff --git a/Graphon.lean b/Graphon.lean
index b460dd5..019857e 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -49,6 +49,7 @@ import Graphon.RelPooledLatents
 import Graphon.RelPooledExtension
 import Graphon.RelPooledAcceptance
 import Graphon.RelRankSuccessorContract
+import Graphon.RelBipartiteRegression
 import Graphon.RelSingletonPeel
 import Graphon.RelFixingAlgebra
 import Graphon.RelRankAlgebra
@@ -269,6 +270,7 @@ 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. The adversarial bipartite and i.i.d. regressions live in a separate shared module
+* `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.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
diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean
index 0777b89..5950d28 100644
--- a/Graphon/RelBipartiteRegression.lean
+++ b/Graphon/RelBipartiteRegression.lean
@@ -710,6 +710,97 @@ theorem measure_xorTrue :
     Fin.prod_univ_two, uniform01_Iic_half, uniform01_Iic_half_compl]
   rw [← add_mul, ENNReal.add_halves, one_mul]
 
+/-! ### Nonindependence
+
+All null-set reasoning lives in one a.e. event-equivalence lemma; the final theorem is purely
+numerical. -/
+
+/-- The latent-side parity event. -/
+def parityEvent : Set (RankLatentSpace digraphSig 2) :=
+  {ω | xor (colour (freshLayer ω) 0) (colour (freshLayer ω) 1) = true}
+
+/-- The structure-side edge event. -/
+def edgeEvent : Set (RelStructure digraphSig (Vinfinite digraphSig)) :=
+  {X | X (digraphCoord 0 1) = true}
+
+theorem measurableSet_parityEvent : MeasurableSet parityEvent :=
+  (Measurable.of_discrete (f := fun p : Bool × Bool => xor p.1 p.2)).comp
+    (((measurable_colour 0).comp measurable_freshLayer).prodMk
+      ((measurable_colour 1).comp measurable_freshLayer)) (measurableSet_singleton true)
+
+theorem measurableSet_edgeEvent : MeasurableSet edgeEvent := by
+  have hset : edgeEvent =
+      (fun X : RelStructure digraphSig (Vinfinite digraphSig) => X (digraphCoord 0 1)) ⁻¹'
+        {true} := rfl
+  rw [hset]
+  exact (measurable_pi_apply _) (measurableSet_singleton true)
+
+/-- **The latent parity event has probability one half**, transported from the two-vertex
+marginal. -/
+theorem measure_parityEvent :
+    rankTwoCoupling (Prod.snd ⁻¹' parityEvent) = 1 / 2 := by
+  have hfun : Measurable
+      (fun (ω : RankLatentSpace digraphSig 2) (d : Fin 2) => freshLayer ω (pairIndex d)) :=
+    measurable_pi_lambda _ fun _ => (measurable_pi_apply _).comp measurable_freshLayer
+  have hxs : MeasurableSet
+      {y : Fin 2 → ℝ | xor (decide (y 0 ≤ 1 / 2)) (decide (y 1 ≤ 1 / 2)) = true} :=
+    (Measurable.of_discrete (f := fun p : Bool × Bool => xor p.1 p.2)).comp
+      ((measurable_decideLe (measurable_pi_apply 0)).prodMk
+        (measurable_decideLe (measurable_pi_apply 1))) (measurableSet_singleton true)
+  have hmap : (rankLatentSource digraphSig 2).map
+      (fun ω d => freshLayer ω (pairIndex d)) = Measure.pi fun _ : Fin 2 => uniform01 := by
+    rw [show (fun (ω : RankLatentSpace digraphSig 2) (d : Fin 2) => freshLayer ω (pairIndex d)) =
+        (fun (x : Colours) (d : Fin 2) => x (pairIndex d)) ∘ freshLayer from rfl,
+      ← Measure.map_map (measurable_pi_lambda _ fun _ => measurable_pi_apply _)
+        measurable_freshLayer, map_freshLayer, source_map_pairIndex]
+  have hpre : parityEvent = (fun ω d => freshLayer ω (pairIndex d)) ⁻¹'
+      {y : Fin 2 → ℝ | xor (decide (y 0 ≤ 1 / 2)) (decide (y 1 ≤ 1 / 2)) = true} := rfl
+  calc rankTwoCoupling (Prod.snd ⁻¹' parityEvent)
+      = (rankTwoCoupling.map Prod.snd) parityEvent :=
+        (Measure.map_apply measurable_snd measurableSet_parityEvent).symm
+    _ = (rankLatentSource digraphSig 2) parityEvent := by rw [rankTwoCoupling_map_snd]
+    _ = ((rankLatentSource digraphSig 2).map fun ω d => freshLayer ω (pairIndex d))
+          {y : Fin 2 → ℝ | xor (decide (y 0 ≤ 1 / 2)) (decide (y 1 ≤ 1 / 2)) = true} := by
+        rw [Measure.map_apply hfun hxs, ← hpre]
+    _ = (Measure.pi fun _ : Fin 2 => uniform01)
+          {y : Fin 2 → ℝ | xor (decide (y 0 ≤ 1 / 2)) (decide (y 1 ≤ 1 / 2)) = true} := by
+        rw [hmap]
+    _ = 1 / 2 := measure_xorTrue
+
+/-- **The one a.e. event equivalence**: the pulled-back edge and parity events agree. -/
+theorem ae_edgeEvent_iff_parityEvent :
+    ∀ᵐ p ∂rankTwoCoupling, (p ∈ Prod.fst ⁻¹' edgeEvent ↔ p ∈ Prod.snd ⁻¹' parityEvent) := by
+  filter_upwards [ae_edge_xor (by norm_num : (0 : ℕ) ≠ 1)] with p hp
+  simp only [Set.mem_preimage, edgeEvent, parityEvent, Set.mem_setOf_eq, hp]
+
+/-- The edge event has probability one half. -/
+theorem measure_edgeEvent : rankTwoCoupling (Prod.fst ⁻¹' edgeEvent) = 1 / 2 := by
+  rw [measure_congr (Filter.eventuallyEq_set.mpr ae_edgeEvent_iff_parityEvent),
+    measure_parityEvent]
+
+/-- Their intersection also has probability one half — they coincide. -/
+theorem measure_edge_inter_parity :
+    rankTwoCoupling (Prod.fst ⁻¹' edgeEvent ∩ Prod.snd ⁻¹' parityEvent) = 1 / 2 := by
+  rw [measure_congr (Filter.EventuallyEq.inter
+      (Filter.eventuallyEq_set.mpr ae_edgeEvent_iff_parityEvent) Filter.EventuallyEq.rfl),
+    Set.inter_self, measure_parityEvent]
+
+/-- **The array is not independent of its new latent layer.** A constant edge would also be "a
+function of the colours"; what rules that out is that `1/2 ≠ 1/4`. -/
+theorem not_indepFun_rankTwoCoupling :
+    ¬ IndepFun (Prod.fst : RelStructure digraphSig (Vinfinite digraphSig) ×
+      RankLatentSpace digraphSig 2 → _) Prod.snd rankTwoCoupling := by
+  intro h
+  have hmul := h.measure_inter_preimage_eq_mul edgeEvent parityEvent
+    measurableSet_edgeEvent measurableSet_parityEvent
+  rw [measure_edge_inter_parity, measure_edgeEvent, measure_parityEvent] at hmul
+  have hne : (1 / 2 : ℝ≥0∞) ≠ 1 / 2 * (1 / 2) := by
+    intro heq
+    have hreal := congrArg ENNReal.toReal heq
+    rw [ENNReal.toReal_mul] at hreal
+    norm_num at hreal
+  exact hne hmul
+
 end BipartiteRegression
 
 end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 514e08a..d13ba32 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -338,6 +338,14 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 -- R4 converse (#107): the shared successor contract (interface only).
 #print axioms RelSignature.InfiniteRelExchangeableLaw.truncation_zero
 #print axioms RelSignature.InfiniteRelExchangeableLaw.austinSuccessor_eq_kallenbergSuccessor
+
+-- R4 converse (#196): the bipartite regression for the successor contract.
+#print axioms RelSignature.BipartiteRegression.bipartiteExchangeable
+#print axioms RelSignature.BipartiteRegression.rankTwoCoupling_truncation
+#print axioms RelSignature.BipartiteRegression.blockMap_pair_arr
+#print axioms RelSignature.BipartiteRegression.bipartiteSuccessor
+#print axioms RelSignature.BipartiteRegression.ae_edge_xor
+#print axioms RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling
 #print axioms MeasureTheory.condExp_comp_measurePreserving
 #print axioms ProbabilityTheory.condExp_set_comp_measurePreserving
 #print axioms ProbabilityTheory.condIndepFun_comp_measurePreserving
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 6738d7d..5835694 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -301,6 +301,12 @@
     "RelSignature.InfiniteRelExchangeableLaw.PooledRankExtension.screening",
     "RelSignature.InfiniteRelExchangeableLaw.truncation_zero",
     "RelSignature.InfiniteRelExchangeableLaw.austinSuccessor_eq_kallenbergSuccessor",
+    "RelSignature.BipartiteRegression.bipartiteExchangeable",
+    "RelSignature.BipartiteRegression.rankTwoCoupling_truncation",
+    "RelSignature.BipartiteRegression.blockMap_pair_arr",
+    "RelSignature.BipartiteRegression.bipartiteSuccessor",
+    "RelSignature.BipartiteRegression.ae_edge_xor",
+    "RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling",
     "MeasureTheory.condExp_comp_measurePreserving",
     "ProbabilityTheory.condExp_set_comp_measurePreserving",
     "ProbabilityTheory.condIndepFun_comp_measurePreserving",

From 62f454c76fcaaa5e08c954fd4cf8084f5931227f Mon Sep 17 00:00:00 2001
From: Cameron Freer <cameronfreer@gmail.com>
Date: Tue, 18 Aug 2026 04:21:09 +0000
Subject: [PATCH 11/11] docs: list uniform01_Iic in its module header; timeless
 regression wording (#196)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

SamplerSources' contents list now mentions uniform01_Iic — the
declaration moved into the authoritative module but its header did not
record it.

The claim that the bipartite and i.i.d. regressions 'live in a separate
shared module' is replaced by 'Adversarial examples are kept in
route-independent regression modules, outside this interface'. The i.i.d.
module does not exist yet, and the plan is separate modules rather than a
shared one, so the previous wording was both premature and wrong about
the layout. Applied consistently in Graphon.lean and the contract
module's own header.
---
 Graphon.lean                          | 2 +-
 Graphon/RelRankSuccessorContract.lean | 4 ++--
 Graphon/SamplerSources.lean           | 3 ++-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/Graphon.lean b/Graphon.lean
index 019857e..4ed861c 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -269,7 +269,7 @@ in Lean 4 using Mathlib.
 * `Graphon.RelPooledLatents` — R4 converse (#107), stage 1 of the pooled-latent extension gate: the core instantiated at `PoolVertex S`. `PooledRankLatentIndex`/`PooledRankLatentSpace`/`pooledRankLatentSource`; `pooledRankLatentRelabel`, the action of the **full mixed** pooled family `∀ s, Equiv.Perm (PoolVertex S s)` — permutations moving vertices between halves included — with its identity and composition laws and exact source invariance; and `restrictOriginalLatents`, the measurable restriction to latents indexed by original supports, whose codomain is the rank-`n` cube itself because the index type is the carrier-parametric one. Naturality is stated in the **honest moved-window form** valid for every pooled permutation, with the commuting square available only as the split corollary. Law-free: no `RankRepresentation`, recovery, screening, or coupling appears, and those enter at later stages of the gate
 * `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. The adversarial bipartite and i.i.d. regressions live in a separate shared module
+* `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.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.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
diff --git a/Graphon/RelRankSuccessorContract.lean b/Graphon/RelRankSuccessorContract.lean
index e04f5c8..2b3834c 100644
--- a/Graphon/RelRankSuccessorContract.lean
+++ b/Graphon/RelRankSuccessorContract.lean
@@ -39,8 +39,8 @@ almost everywhere and not up to isomorphism.
   (`PooledRankExtension.map_restrict_embedding`); each route's **intermediate** construction is
   required to consume it, rather than a vacuous check being added at this interface.
 
-The adversarial regressions belong in a separate shared module, so that this file stays
-interface-only and free of the heavier imports they need.
+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.
 -/
 
 open MeasureTheory
diff --git a/Graphon/SamplerSources.lean b/Graphon/SamplerSources.lean
index 6d52d76..dca4937 100644
--- a/Graphon/SamplerSources.lean
+++ b/Graphon/SamplerSources.lean
@@ -17,7 +17,8 @@ generically (no graph/digraph-specific index types) so the directed sampler need
 
 * `OffDiagPairIndex V` — the generic off-diagonal unordered-pair index (one uniform per pair of
   distinct vertices); `InfiniteGraph.EdgeIndex` is definitionally `OffDiagPairIndex ℕ`;
-* `uniform01` — the uniform probability measure on `[0,1]`;
+* `uniform01` — the uniform probability measure on `[0,1]`, with `uniform01_Iic` giving the mass
+  of an initial segment;
 * `iidVertexSource μ` — i.i.d. positions `ℕ → α` with law `μ` (via `Measure.infinitePi`);
 * `iidUniformSource ι` — i.i.d. uniforms on `[0,1]` indexed by an arbitrary type `ι`;
 * `Measure.infinitePi_map_comp_equiv` — invariance/reindexing under an index equivalence;