From a70369e09e4b5582267b7b7a2e40aaf4a2698d58 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Tue, 18 Aug 2026 04:44:54 +0000 Subject: [PATCH 01/11] wip(#196): the symmetric i.i.d.-edge law One uniform per two-point support, with the array keyed by a coordinate's SUPPORT. That makes both required facts definitional: X_uv and X_vu share a support and hence a value, and the diagonal has a one-element support so it falls in the false branch. Blocks at distinct two-point supports are i.i.d., being distinct source coordinates. No equivariant-orientation problem arises, because the directed coordinates are never given independent values. measurable_decideLe promoted from the bipartite regression to SamplerSources: thresholding a measurable real is general infrastructure and now has a genuine second consumer, which is the condition for extracting it. The two regression modules stay independent of each other. --- Graphon/RelBipartiteRegression.lean | 14 ---- Graphon/RelIidEdgeRegression.lean | 109 ++++++++++++++++++++++++++++ Graphon/SamplerSources.lean | 16 +++- 3 files changed, 124 insertions(+), 15 deletions(-) create mode 100644 Graphon/RelIidEdgeRegression.lean diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean index 5950d28..5bd9eea 100644 --- a/Graphon/RelBipartiteRegression.lean +++ b/Graphon/RelBipartiteRegression.lean @@ -62,20 +62,6 @@ 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] -/-- 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 diff --git a/Graphon/RelIidEdgeRegression.lean b/Graphon/RelIidEdgeRegression.lean new file mode 100644 index 0000000..c06bad7 --- /dev/null +++ b/Graphon/RelIidEdgeRegression.lean @@ -0,0 +1,109 @@ +/- +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 i.i.d.-edge regression for the successor contract (R4 converse, #107, #196) + +A hand-built rank `2 → 3` successor witness over `digraphSig`, testing **staging and recovery** +together — where the bipartite regression tested independence and symmetry. + +The law is the symmetric i.i.d.-edge law: one uniform per two-point support, with + +`X_uv = X_vu = 1{U_{u,v} ≤ 1/2}` and `X_uu = false`. + +Keying the array by a coordinate's *support* makes both facts definitional: the two directed +coordinates of a block share a support and therefore a value, and the diagonal has a one-element +support so it falls in the default branch. Blocks at **distinct** two-point supports are i.i.d., +being distinct coordinates of the source. Making `X_uv` and `X_vu` independently directed would +introduce an equivariant-orientation problem without testing staging any better. + +## Shape of the regression + +* the rank-two coupling is defined **independently** as `iidEdgeLaw.prod (rankLatentSource 2)`, + so independence of the edges from the old latents is literal; +* the rank-three coupling is built from `rankLatentSource 3`, retaining the whole latent point and + decoding the array from its fresh rank-two layer; +* the truncation identity is proved immediately, before either representation is packaged. +-/ + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace RelSignature + +namespace IidEdgeRegression + +/-- The edge layer: one uniform per two-point support. -/ +abbrev Edges := RankSupport digraphSig 2 → ℝ + +open scoped Classical in +/-- **The symmetric i.i.d.-edge array**, keyed by a coordinate's support. Both directed +coordinates of a two-point block share a support, hence a value; the diagonal has a one-element +support and is `false`. -/ +noncomputable def arr (e : Edges) : RelStructure digraphSig (Vinfinite digraphSig) := + fun c => if h : c.support.card = 2 then decide (e ⟨c.support, h⟩ ≤ 1 / 2) else false + +open scoped Classical in +/-- **Symmetry is definitional**: the two directed coordinates of a block share a support. -/ +theorem arr_symm (e : Edges) (u v : ℕ) : + arr e (digraphCoord u v) = arr e (digraphCoord v u) := by + have hsupp : (digraphCoord u v : RelCoord digraphSig (Vinfinite digraphSig)).support = + (digraphCoord v u : RelCoord digraphSig (Vinfinite digraphSig)).support := by + refine Finset.ext fun w => ?_ + rw [RelCoord.mem_support_iff, RelCoord.mem_support_iff] + constructor + · rintro ⟨i, rfl⟩ + fin_cases i + · exact ⟨1, rfl⟩ + · exact ⟨0, rfl⟩ + · rintro ⟨i, rfl⟩ + fin_cases i + · exact ⟨1, rfl⟩ + · exact ⟨0, rfl⟩ + simp only [arr, hsupp] + +open scoped Classical in +/-- **The diagonal is `false`**: its support has one element, not two. -/ +@[simp] theorem arr_diagonal (e : Edges) (v : ℕ) : arr e (digraphCoord v v) = false := by + have hsupp : (digraphCoord v v : RelCoord digraphSig (Vinfinite digraphSig)).support = + {⟨(), v⟩} := by + refine Finset.ext fun w => ?_ + rw [RelCoord.mem_support_iff, Finset.mem_singleton] + constructor + · rintro ⟨i, rfl⟩ + fin_cases i <;> rfl + · rintro rfl + exact ⟨0, rfl⟩ + rw [arr, dif_neg] + rw [hsupp, Finset.card_singleton] + omega + +open scoped Classical in +theorem measurable_arr : Measurable arr := by + refine measurable_pi_lambda _ fun c => ?_ + by_cases h : (c : RelCoord digraphSig (Vinfinite digraphSig)).support.card = 2 + · have hfun : (fun e : Edges => arr e c) = fun e => decide (e ⟨c.support, h⟩ ≤ 1 / 2) := by + funext e; rw [arr, dif_pos h] + rw [hfun] + exact measurable_decideLe (measurable_pi_apply _) + · have hfun : (fun e : Edges => arr e c) = fun _ => false := by + funext e; rw [arr, dif_neg h] + rw [hfun] + exact measurable_const + +/-- **The i.i.d.-edge law**, defined from the edge layer alone. -/ +noncomputable def iidEdgeLaw : Measure (RelStructure digraphSig (Vinfinite digraphSig)) := + (iidUniformSource (RankSupport digraphSig 2)).map arr + +instance : IsProbabilityMeasure iidEdgeLaw := + Measure.isProbabilityMeasure_map measurable_arr.aemeasurable + +end IidEdgeRegression + +end RelSignature diff --git a/Graphon/SamplerSources.lean b/Graphon/SamplerSources.lean index dca4937..40e3e0b 100644 --- a/Graphon/SamplerSources.lean +++ b/Graphon/SamplerSources.lean @@ -18,7 +18,7 @@ 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]`, with `uniform01_Iic` giving the mass - of an initial segment; + of an initial segment, and `measurable_decideLe` the measurability of thresholding at `1/2`; * `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; @@ -70,6 +70,20 @@ instance : IsProbabilityMeasure uniform01 := ⟨by rw [uniform01, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter, Real.volume_Icc]; norm_num⟩ +/-- 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 + /-- 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 From b0c67e7f22d02648403c59ae8dba92df2b09b7a2 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Tue, 18 Aug 2026 04:45:53 +0000 Subject: [PATCH 02/11] wip(#196): both i.i.d.-edge couplings and the truncation gate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit rankTwoCoupling := iidEdgeLaw.prod (rankLatentSource 2) — a product, so independence of the edges from the old latents is literal rather than argued. rankThreeCoupling is built from rankLatentSource 3, retaining the whole latent point and decoding the array from its fresh rank-two layer. rankThreeCoupling_truncation is proved immediately, before either representation is packaged: the fresh edge layer splits off from the old latents, the array reads only the former and the truncation only the latter. It went through on the first attempt, the bipartite version having established the rewrite pattern. --- Graphon/RelIidEdgeRegression.lean | 86 +++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) diff --git a/Graphon/RelIidEdgeRegression.lean b/Graphon/RelIidEdgeRegression.lean index c06bad7..76ad354 100644 --- a/Graphon/RelIidEdgeRegression.lean +++ b/Graphon/RelIidEdgeRegression.lean @@ -104,6 +104,92 @@ noncomputable def iidEdgeLaw : Measure (RelStructure digraphSig (Vinfinite digra instance : IsProbabilityMeasure iidEdgeLaw := Measure.isProbabilityMeasure_map measurable_arr.aemeasurable +/-! ### The two couplings, described independently + +The rank-two coupling is a product, so independence of the edges from the old latents is literal. +The rank-three coupling is built from the rank-three source and decodes the array from its fresh +rank-two layer. The truncation identity is proved immediately, before either representation is +packaged. -/ + +/-- **The rank-two coupling**: the i.i.d.-edge law together with an *independent* rank-two latent +array. Defined without reference to the rank-three object. -/ +noncomputable def rankTwoCoupling : + Measure (RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 2) := + iidEdgeLaw.prod (rankLatentSource digraphSig 2) + +instance : IsProbabilityMeasure rankTwoCoupling := by + rw [rankTwoCoupling]; infer_instance + +@[simp] theorem rankTwoCoupling_map_fst : rankTwoCoupling.map Prod.fst = iidEdgeLaw := by + rw [rankTwoCoupling, Measure.map_fst_prod]; simp + +@[simp] theorem rankTwoCoupling_map_snd : + rankTwoCoupling.map Prod.snd = rankLatentSource digraphSig 2 := by + rw [rankTwoCoupling, Measure.map_snd_prod]; simp + +/-- The fresh rank-two layer of a rank-three latent point. -/ +noncomputable def freshLayer (ω : RankLatentSpace digraphSig 3) : Edges := + (rankLatentSpaceSuccEquiv 2 ω).2 + +theorem measurable_freshLayer : Measurable freshLayer := + (rankLatentSpaceSuccEquiv 2).measurable.snd + +theorem map_freshLayer : + (rankLatentSource digraphSig 3).map freshLayer = + iidUniformSource (RankSupport digraphSig 2) := by + have hfl : freshLayer = Prod.snd ∘ (rankLatentSpaceSuccEquiv 2) := rfl + rw [hfl, ← Measure.map_map measurable_snd (rankLatentSpaceSuccEquiv 2).measurable, + rankLatentSource_map_rankLatentSpaceSuccEquiv, Measure.map_snd_prod] + simp + +/-- **The rank-three coupling**: the array is decoded from the fresh rank-two layer, and the whole +rank-three latent point is retained. -/ +noncomputable def rankThreeCoupling : + Measure (RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 3) := + (rankLatentSource digraphSig 3).map fun ω => (arr (freshLayer ω), ω) + +theorem measurable_rankThreeMap : + Measurable fun ω : RankLatentSpace digraphSig 3 => (arr (freshLayer ω), ω) := + (measurable_arr.comp measurable_freshLayer).prodMk measurable_id + +instance : IsProbabilityMeasure rankThreeCoupling := by + rw [rankThreeCoupling] + exact Measure.isProbabilityMeasure_map measurable_rankThreeMap.aemeasurable + +@[simp] theorem rankThreeCoupling_map_fst : rankThreeCoupling.map Prod.fst = iidEdgeLaw := by + rw [rankThreeCoupling, Measure.map_map measurable_fst measurable_rankThreeMap, + show (Prod.fst ∘ fun ω : RankLatentSpace digraphSig 3 => (arr (freshLayer ω), ω)) = + arr ∘ freshLayer from rfl, + ← Measure.map_map measurable_arr measurable_freshLayer, map_freshLayer, iidEdgeLaw] + +@[simp] theorem rankThreeCoupling_map_snd : + rankThreeCoupling.map Prod.snd = rankLatentSource digraphSig 3 := by + rw [rankThreeCoupling, Measure.map_map measurable_snd measurable_rankThreeMap, + show (Prod.snd ∘ fun ω : RankLatentSpace digraphSig 3 => (arr (freshLayer ω), ω)) = id from rfl, + Measure.map_id] + +/-- **The truncation identity — the gate**: truncating the rank-three coupling's latents to rank +two returns the *independently defined* rank-two coupling. The fresh edge layer splits off from +the old latents, the array reads only the former and the truncation only the latter. -/ +theorem rankThreeCoupling_truncation : + rankThreeCoupling.map (Prod.map id (rankLatentProjection (S := digraphSig) (Nat.le_succ 2))) = + rankTwoCoupling := by + rw [rankThreeCoupling, + Measure.map_map (measurable_id.prodMap + (measurable_rankLatentProjection (S := digraphSig) (Nat.le_succ 2))) + measurable_rankThreeMap, + show (Prod.map (id : RelStructure digraphSig (Vinfinite digraphSig) → _) + (rankLatentProjection (S := digraphSig) (Nat.le_succ 2)) ∘ + fun ω : RankLatentSpace digraphSig 3 => (arr (freshLayer ω), ω)) = + (Prod.map arr (id : RankLatentSpace digraphSig 2 → _)) ∘ Prod.swap ∘ + (rankLatentSpaceSuccEquiv 2) from rfl, + ← Measure.map_map (measurable_arr.prodMap measurable_id) + (measurable_swap.comp (rankLatentSpaceSuccEquiv 2).measurable), + ← Measure.map_map measurable_swap (rankLatentSpaceSuccEquiv 2).measurable, + rankLatentSource_map_rankLatentSpaceSuccEquiv, Measure.prod_swap, + ← Measure.map_prod_map _ _ measurable_arr measurable_id, Measure.map_id, + rankTwoCoupling, iidEdgeLaw] + end IidEdgeRegression end RelSignature From b82a07268838d28b376aefe11d7963d668262228 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 19 Aug 2026 13:14:48 +0000 Subject: [PATCH 03/11] feat: cond-indep-from-product lemma for the i.i.d.-edge regression (#196) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `condIndepFun_of_prod_right`: on a product space, a function of the first coordinate is conditionally independent of a function of the second given any sub-algebra of the second coordinate's algebra. This is the screening engine for the rank-two representation, where the old latents live in the second factor and the edges are decoded from the first. Two elaboration notes worth keeping: * `CondIndepFun` takes the conditioning algebra *before* the ambient one, so the statement is written in explicit `@` form. * An abstract `{m' : MeasurableSpace (α × β)}` binder enters local instance search and shadows `Prod.instMeasurableSpace`, so the proof opens with `letI mΩ : MeasurableSpace (α × β) := Prod.instMeasurableSpace` and annotates the standalone projections (`Prod.fst : α × β → α`). Kept private here; recorded as a Provisional upstream candidate on #160. --- Graphon/RelIidEdgeRegression.lean | 88 +++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) diff --git a/Graphon/RelIidEdgeRegression.lean b/Graphon/RelIidEdgeRegression.lean index 76ad354..97cf836 100644 --- a/Graphon/RelIidEdgeRegression.lean +++ b/Graphon/RelIidEdgeRegression.lean @@ -6,6 +6,7 @@ Authors: Cameron Freer import Graphon.RelRankSuccessorContract import Graphon.InfiniteDigraph import Graphon.ForMathlib.CondIndepSup +import Mathlib.Probability.ConditionalExpectation /-! # The i.i.d.-edge regression for the successor contract (R4 converse, #107, #196) @@ -104,6 +105,93 @@ noncomputable def iidEdgeLaw : Measure (RelStructure digraphSig (Vinfinite digra instance : IsProbabilityMeasure iidEdgeLaw := Measure.isProbabilityMeasure_map measurable_arr.aemeasurable +/-! ### The product-right conditional-independence lemma + +Kept **private**: it has one consumer (rank-two screening below), which is below the promotion bar +for `Graphon/ForMathlib/`. Neither Mathlib nor TauCeti has it — `condExp_indep_eq` supplies the +constant conditional expectation of a left-coordinate observation, but not the intersection +identity that conditional independence needs. Recorded as a prospective upstream candidate. + +Stated for an arbitrary conditioning σ-algebra below `comap Prod.snd`, so conditioning on a +function of the right coordinate is a corollary rather than the definition. + +Two elaboration points are load-bearing. `CondIndepFun` takes the conditioning algebra *before* the +ambient measurable space, so the conclusion is written in explicit `@` form. And an abstract +`m' : MeasurableSpace (α × β)` binder **enters local instance search**, shadowing the product +instance throughout the proof body; the opening `letI` restores the intended ambient instance +without weakening the statement. -/ + +private theorem comap_fst_le_prod {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : + MeasurableSpace.comap (Prod.fst : α × β → α) inferInstance ≤ + (Prod.instMeasurableSpace : MeasurableSpace (α × β)) := by + rintro S ⟨T, hT, rfl⟩ + exact measurable_fst hT + +private theorem comap_snd_le_prod {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : + MeasurableSpace.comap (Prod.snd : α × β → β) inferInstance ≤ + (Prod.instMeasurableSpace : MeasurableSpace (α × β)) := by + rintro S ⟨T, hT, rfl⟩ + exact measurable_snd hT + +open scoped Classical in +/-- Under a product measure, a left-coordinate observation is conditionally independent of a +right-coordinate observation given **any** σ-algebra below the right coordinate's. -/ +private theorem condIndepFun_of_prod_right {α β γ δ : Type*} + [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] + [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty α] [Nonempty β] + {μ : Measure α} {ν : Measure β} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] + {m' : MeasurableSpace (α × β)} + (hm' : m' ≤ MeasurableSpace.comap (Prod.snd : α × β → β) inferInstance) + {f : α → γ} {g : β → δ} (hf : Measurable f) (hg : Measurable g) : + @ProbabilityTheory.CondIndepFun (α × β) m' Prod.instMeasurableSpace + (StandardBorelSpace.prod) (hm'.trans comap_snd_le_prod) + γ δ inferInstance inferInstance + (f ∘ (Prod.fst : α × β → α)) (g ∘ (Prod.snd : α × β → β)) (μ.prod ν) inferInstance := by + letI mΩ : MeasurableSpace (α × β) := Prod.instMeasurableSpace + have hmAmbient : m' ≤ (Prod.instMeasurableSpace : MeasurableSpace (α × β)) := + hm'.trans comap_snd_le_prod + have hfst : Measurable (f ∘ (Prod.fst : α × β → α)) := hf.comp measurable_fst + have hsnd : Measurable (g ∘ (Prod.snd : α × β → β)) := hg.comp measurable_snd + have hcoord : Indep (MeasurableSpace.comap (Prod.fst : α × β → α) inferInstance) + (MeasurableSpace.comap (Prod.snd : α × β → β) inferInstance) (μ.prod ν) := + indepFun_prod measurable_id measurable_id + rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hfst hsnd] + intro s t hs ht + set A : Set (α × β) := (f ∘ (Prod.fst : α × β → α)) ⁻¹' s with hAdef + set B : Set (α × β) := (g ∘ (Prod.snd : α × β → β)) ⁻¹' t with hBdef + have hAmem : MeasurableSet[MeasurableSpace.comap (Prod.fst : α × β → α) inferInstance] A := + ⟨f ⁻¹' s, hf hs, rfl⟩ + have hBmem : MeasurableSet[MeasurableSpace.comap (Prod.snd : α × β → β) inferInstance] B := + ⟨g ⁻¹' t, hg ht, rfl⟩ + have hAmeas : MeasurableSet A := hfst hs + have hBmeas : MeasurableSet B := hsnd ht + have hAconst : (μ.prod ν)⟦A | m'⟧ =ᵐ[μ.prod ν] fun _ => ((μ.prod ν) A).toReal := by + have hInd : Indep (MeasurableSpace.comap (Prod.fst : α × β → α) inferInstance) m' + (μ.prod ν) := indep_of_indep_of_le_right hcoord hm' + refine (condExp_indep_eq (μ := μ.prod ν) comap_fst_le_prod hmAmbient + (stronglyMeasurable_const.indicator hAmem) hInd).trans + (Filter.Eventually.of_forall fun _ => ?_) + rw [integral_indicator_const (1 : ℝ) hAmeas, smul_eq_mul, mul_one, measureReal_def] + have hInter : (μ.prod ν)⟦A ∩ B | m'⟧ =ᵐ[μ.prod ν] + fun ω => ((μ.prod ν) A).toReal * ((μ.prod ν)⟦B | m'⟧) ω := by + refine (ae_eq_condExp_of_forall_setIntegral_eq hmAmbient + ((integrable_const (1 : ℝ)).indicator (hAmeas.inter hBmeas)) + (fun S _ _ => (integrable_condExp.const_mul _).integrableOn) + (fun S hSm _ => ?_) (stronglyMeasurable_condExp.const_mul _).aestronglyMeasurable).symm + have hSamb : MeasurableSet S := hmAmbient _ hSm + have hmul : (μ.prod ν) (A ∩ (S ∩ B)) = (μ.prod ν) A * (μ.prod ν) (S ∩ B) := by + simpa using hcoord A (S ∩ B) hAmem ((hm' _ hSm).inter hBmem) + rw [integral_const_mul, + setIntegral_condExp hmAmbient ((integrable_const (1 : ℝ)).indicator hBmeas) hSm, + setIntegral_indicator hBmeas, setIntegral_indicator (hAmeas.inter hBmeas), + integral_const, integral_const, measureReal_restrict_apply_univ, + measureReal_restrict_apply_univ, + show S ∩ (A ∩ B) = A ∩ (S ∩ B) from Set.inter_left_comm _ _ _, + measureReal_def, measureReal_def, hmul, ENNReal.toReal_mul] + ring + filter_upwards [hInter, hAconst] with ω h1 h2 + rw [h1, h2] + /-! ### The two couplings, described independently The rank-two coupling is a product, so independence of the edges from the old latents is literal. From 8ab810589a246dd1f423024eb88980fe1d80384b Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 19 Aug 2026 13:17:50 +0000 Subject: [PATCH 04/11] refactor: generic sortwise-permutation action on rank supports (#196) `rankSupportPerm` acts by an arbitrary sortwise permutation, not only a finitely supported one: cardinality is preserved by injectivity alone, and a law's exchangeability is invariance under *all* sortwise permutations. `rankSupportEquiv` is now its finitely supported instance, and the bipartite regression's rank-one `supportPerm` is a wrapper rather than a third hand-written copy. Definitionally unchanged in both cases, so the existing `show`-style proofs are untouched. --- Graphon/RelBipartiteRegression.lean | 29 +++------------------- Graphon/RelRankSuccessor.lean | 38 ++++++++++++++++++++--------- 2 files changed, 30 insertions(+), 37 deletions(-) diff --git a/Graphon/RelBipartiteRegression.lean b/Graphon/RelBipartiteRegression.lean index 5bd9eea..9cc9ac6 100644 --- a/Graphon/RelBipartiteRegression.lean +++ b/Graphon/RelBipartiteRegression.lean @@ -83,32 +83,11 @@ theorem measurable_arr : Measurable arr := by /-! ### The relabeling action on the fresh layer -/ -open scoped Classical in -/-- A permutation of the vertices permutes the singleton supports. -/ +/-- A permutation of the vertices permutes the singleton supports — the rank-one instance of the +generic `rankSupportPerm`. -/ 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]) + RankSupport digraphSig 1 ≃ RankSupport digraphSig 1 := + rankSupportPerm (fun _ : Unit => σ) 1 open scoped Classical in @[simp] theorem supportPerm_vertexSupport (σ : Equiv.Perm ℕ) (v : ℕ) : diff --git a/Graphon/RelRankSuccessor.lean b/Graphon/RelRankSuccessor.lean index 0c0e995..31bc18e 100644 --- a/Graphon/RelRankSuccessor.lean +++ b/Graphon/RelRankSuccessor.lean @@ -84,33 +84,47 @@ theorem card_image_sigmaMap {A : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ} exact hA open scoped Classical in -/-- A relabeling permutes the supports of each rank. -/ -noncomputable def rankSupportEquiv (σ : FinSuppPerm S) (n : ℕ) : +/-- **An arbitrary sortwise permutation permutes the supports of each rank.** Finite support is +irrelevant here: only injectivity is used, and that is what preserves cardinality. Stated for +arbitrary sortwise permutations because the exchangeability of a law is an invariance under *all* +of them, not only the finitely supported ones. -/ +noncomputable def rankSupportPerm (σ : ∀ s, Equiv.Perm (Vinfinite S s)) (n : ℕ) : RankSupport S n ≃ RankSupport S n where - toFun A := ⟨A.1.image (Sigma.map id fun s => ⇑(σ.1 s)), by + toFun A := ⟨A.1.image (Sigma.map id fun s => ⇑(σ s)), by rw [Finset.card_image_of_injective _ - (Function.injective_id.sigma_map fun s => (σ.1 s).injective)] + (Function.injective_id.sigma_map fun s => (σ s).injective)] exact A.2⟩ - invFun A := ⟨A.1.image (Sigma.map id fun s => ⇑(σ.1 s)⁻¹), by + invFun A := ⟨A.1.image (Sigma.map id fun s => ⇑(σ s)⁻¹), by rw [Finset.card_image_of_injective _ - (Function.injective_id.sigma_map fun s => ((σ.1 s)⁻¹).injective)] + (Function.injective_id.sigma_map fun s => ((σ s)⁻¹).injective)] exact A.2⟩ left_inv A := Subtype.ext (by - show (A.1.image (Sigma.map id fun s => ⇑(σ.1 s))).image (Sigma.map id fun s => ⇑(σ.1 s)⁻¹) + show (A.1.image (Sigma.map id fun s => ⇑(σ s))).image (Sigma.map id fun s => ⇑(σ s)⁻¹) = A.1 rw [Finset.image_image] refine (Finset.image_congr fun v _ => ?_).trans A.1.image_id obtain ⟨s, x⟩ := v - show (⟨s, (σ.1 s)⁻¹ ((σ.1 s) x)⟩ : Σ s : S.Srt, Vinfinite S s) = ⟨s, x⟩ - rw [show (σ.1 s)⁻¹ ((σ.1 s) x) = x from (σ.1 s).symm_apply_apply 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]) right_inv A := Subtype.ext (by - show (A.1.image (Sigma.map id fun s => ⇑(σ.1 s)⁻¹)).image (Sigma.map id fun s => ⇑(σ.1 s)) + show (A.1.image (Sigma.map id fun s => ⇑(σ s)⁻¹)).image (Sigma.map id fun s => ⇑(σ s)) = A.1 rw [Finset.image_image] refine (Finset.image_congr fun v _ => ?_).trans A.1.image_id obtain ⟨s, x⟩ := v - show (⟨s, (σ.1 s) ((σ.1 s)⁻¹ x)⟩ : Σ s : S.Srt, Vinfinite S s) = ⟨s, x⟩ - rw [show (σ.1 s) ((σ.1 s)⁻¹ x) = x from (σ.1 s).apply_symm_apply x]) + show (⟨s, (σ s) ((σ s)⁻¹ x)⟩ : Σ s : S.Srt, Vinfinite S s) = ⟨s, x⟩ + rw [show (σ s) ((σ s)⁻¹ x) = x from (σ s).apply_symm_apply x]) + +open scoped Classical in +@[simp] theorem rankSupportPerm_coe (σ : ∀ s, Equiv.Perm (Vinfinite S s)) (n : ℕ) + (A : RankSupport S n) : + (rankSupportPerm σ n A).1 = A.1.image (Sigma.map id fun s => ⇑(σ s)) := rfl + +open scoped Classical in +/-- A relabeling permutes the supports of each rank — the finitely supported case. -/ +noncomputable def rankSupportEquiv (σ : FinSuppPerm S) (n : ℕ) : + RankSupport S n ≃ RankSupport S n := + rankSupportPerm σ.1 n open scoped Classical in From 2e2e49aff47b3874b4888b13156f13899c9ebde9 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 19 Aug 2026 13:30:05 +0000 Subject: [PATCH 05/11] feat: equivariance and exchangeability of the i.i.d.-edge law (#196) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Relabeling the vertices reindexes the edge layer: a coordinate's support transports covariantly and injectivity preserves its cardinality, so `arr (e ∘ rankSupportPerm σ 2) = RelStructure.relabel σ (arr e)`. Exchangeability is then invariance of an i.i.d. product under a coordinate permutation, and `iidEdgeExchangeable` packages the law. `mem_rankSupportPerm` is stated **without an image** so that no `DecidableEq` instance appears in its type. Over a concrete carrier the natural instance (`instDecidableEqNat`) is not definitionally the classical one used to form the image, which makes `rankSupportPerm_coe` unusable there; the membership form is instance-agnostic. Stated in the abstract-signature file, where no natural instance exists to compete. --- Graphon/RelIidEdgeRegression.lean | 69 +++++++++++++++++++++++++++++++ Graphon/RelRankSuccessor.lean | 10 +++++ 2 files changed, 79 insertions(+) diff --git a/Graphon/RelIidEdgeRegression.lean b/Graphon/RelIidEdgeRegression.lean index 97cf836..2cb3fd2 100644 --- a/Graphon/RelIidEdgeRegression.lean +++ b/Graphon/RelIidEdgeRegression.lean @@ -105,6 +105,75 @@ noncomputable def iidEdgeLaw : Measure (RelStructure digraphSig (Vinfinite digra instance : IsProbabilityMeasure iidEdgeLaw := Measure.isProbabilityMeasure_map measurable_arr.aemeasurable +/-! ### Equivariance and exchangeability + +Relabeling the vertices reindexes the edge layer along `rankSupportPerm`, because a coordinate's +support transports covariantly and its cardinality is preserved. Exchangeability is then the +invariance of an i.i.d. product under a coordinate permutation. -/ + +open scoped Classical in +set_option maxHeartbeats 400000 in +/-- **Equivariance of the array**: relabeling the vertices is reindexing the edge layer. -/ +theorem arr_comp_supportPerm (σ : ∀ _ : Unit, Equiv.Perm ℕ) (e : Edges) : + arr (fun A => e (rankSupportPerm σ 2 A)) = RelStructure.relabel σ (arr e) := by + funext c + have hinj : Function.Injective (Sigma.map id (fun s => ⇑(σ s)) : + (Σ s : Unit, Vinfinite digraphSig s) → Σ s : Unit, Vinfinite digraphSig s) := + Function.injective_id.sigma_map fun s => (σ s).injective + have hmem : ∀ v, v ∈ (RelCoord.map (fun s => ⇑(σ s)) c).support ↔ + ∃ a ∈ c.support, Sigma.map id (fun s => ⇑(σ s)) a = v := by + intro v + constructor + · intro hv + obtain ⟨i, hi⟩ := (RelCoord.mem_support_iff _ _).mp hv + exact ⟨c.taggedValue i, (RelCoord.mem_support_iff _ _).mpr ⟨i, rfl⟩, hi⟩ + · rintro ⟨a, ha, hav⟩ + obtain ⟨i, hi⟩ := (RelCoord.mem_support_iff _ _).mp ha + refine (RelCoord.mem_support_iff _ _).mpr ⟨i, ?_⟩ + rw [← hav, ← hi] + rfl + have hcard : (RelCoord.map (fun s => ⇑(σ s)) c).support.card = c.support.card := by + refine Finset.card_nbij' (Sigma.map id fun s => ⇑(σ s)⁻¹) (Sigma.map id fun s => ⇑(σ s)) + (fun v hv => ?_) (fun v hv => ?_) (fun v hv => ?_) (fun v hv => ?_) + · obtain ⟨a, ha, rfl⟩ := (hmem v).mp hv + obtain ⟨s, x⟩ := a + simpa [Sigma.map] using ha + · exact (hmem _).mpr ⟨v, hv, rfl⟩ + · obtain ⟨a, _, rfl⟩ := (hmem v).mp hv + obtain ⟨s, x⟩ := a + simp [Sigma.map] + · obtain ⟨s, x⟩ := v + simp [Sigma.map] + show arr (fun A => e (rankSupportPerm σ 2 A)) c = arr e (RelCoord.map (fun s => ⇑(σ s)) c) + simp only [arr] + split_ifs with h₁ h₂ h₂ + · refine congrArg (fun r : ℝ => decide (r ≤ 1 / 2)) (congrArg e (Subtype.ext ?_)) + refine Finset.ext fun v => ?_ + exact (mem_rankSupportPerm σ 2 (Subtype.mk c.support h₁ : RankSupport digraphSig 2) v).trans + (hmem v).symm + · exact absurd (hcard.trans h₁) h₂ + · exact absurd (hcard.symm.trans h₂) h₁ + · rfl + +/-- **Exchangeability**: the law is invariant under every sortwise relabeling. -/ +theorem iidEdgeLaw_map_relabel (σ : ∀ _ : Unit, Equiv.Perm ℕ) : + iidEdgeLaw.map (RelStructure.relabel σ) = iidEdgeLaw := by + rw [iidEdgeLaw, Measure.map_map (measurable_relabel σ) measurable_arr, + show RelStructure.relabel σ ∘ arr = + arr ∘ (fun e : Edges => fun A => e (rankSupportPerm σ 2 A)) from by + funext e + exact (arr_comp_supportPerm σ e).symm, + ← Measure.map_map measurable_arr + (measurable_pi_lambda _ fun _ => measurable_pi_apply _), + iidUniformSource, + Measure.infinitePi_map_comp_equiv (fun _ : RankSupport digraphSig 2 => uniform01) + (rankSupportPerm σ 2)] + +/-- The i.i.d.-edge law as an exchangeable law on the infinite structure space. -/ +noncomputable def iidEdgeExchangeable : InfiniteRelExchangeableLaw digraphSig where + law := ⟨iidEdgeLaw, inferInstance⟩ + exchangeable := iidEdgeLaw_map_relabel + /-! ### The product-right conditional-independence lemma Kept **private**: it has one consumer (rank-two screening below), which is below the promotion bar diff --git a/Graphon/RelRankSuccessor.lean b/Graphon/RelRankSuccessor.lean index 31bc18e..96072bd 100644 --- a/Graphon/RelRankSuccessor.lean +++ b/Graphon/RelRankSuccessor.lean @@ -120,6 +120,16 @@ open scoped Classical in (A : RankSupport S n) : (rankSupportPerm σ n A).1 = A.1.image (Sigma.map id fun s => ⇑(σ s)) := rfl +open scoped Classical in +/-- Membership in a permuted support, stated **without an image** so that no `DecidableEq` +instance appears in the type. Consumers over a concrete carrier have a natural instance that is +not definitionally the classical one used to form the image, and `rankSupportPerm_coe` is then +unusable there; this form is not. -/ +theorem mem_rankSupportPerm (σ : ∀ s, Equiv.Perm (Vinfinite S s)) (n : ℕ) (A : RankSupport S n) + (v : Σ s : S.Srt, Vinfinite S s) : + v ∈ (rankSupportPerm σ n A).1 ↔ ∃ a ∈ A.1, Sigma.map id (fun s => ⇑(σ s)) a = v := by + rw [rankSupportPerm_coe, Finset.mem_image] + open scoped Classical in /-- A relabeling permutes the supports of each rank — the finitely supported case. -/ noncomputable def rankSupportEquiv (σ : FinSuppPerm S) (n : ℕ) : From 0251ca219a1a1bb25fd6d6867b3e4eadfa74bae6 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 19 Aug 2026 13:42:05 +0000 Subject: [PATCH 06/11] feat: rank-two invariance/recovery and the full rank-three clauses (#196) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two pointwise block lemmas carry everything: a block whose support does not have two elements is constant `false`, and a block at a two-point support reads exactly the edge coordinate keyed by that support. Rank two: invariance is a product of two invariant factors; recovery below rank two is a constant decoder that reads no latent. Rank three: recovery is the substantive staging clause — a two-point block is decoded from the latent coordinate at its own support, which the rank-three array carries because 2 < 3. Screening at a three-point support is vacuous: over a binary signature no coordinate reads three vertices, so the block space is a single point. `RelCoord.card_support_le` is stated over an abstract carrier for the same reason as `mem_rankSupportPerm`: no natural `DecidableEq` competes with the classical instance used to form the support's image. --- Graphon/RelEqualityPattern.lean | 8 ++ Graphon/RelIidEdgeRegression.lean | 138 ++++++++++++++++++++++++++++++ 2 files changed, 146 insertions(+) diff --git a/Graphon/RelEqualityPattern.lean b/Graphon/RelEqualityPattern.lean index cb1b615..803f335 100644 --- a/Graphon/RelEqualityPattern.lean +++ b/Graphon/RelEqualityPattern.lean @@ -93,6 +93,14 @@ theorem RelCoord.mem_support_iff (c : RelCoord S V) (v : Σ s : S.Srt, V s) : v ∈ c.support ↔ ∃ i, c.taggedValue i = v := by simp [RelCoord.support] +open scoped Classical in +/-- **The support is no larger than the arity**: it is the image of the finitely many positions. +Stated over an abstract carrier, where no natural `DecidableEq` competes with the classical +instance used to form the image. -/ +theorem RelCoord.card_support_le (c : RelCoord S V) : c.support.card ≤ S.arity c.1 := by + refine le_trans Finset.card_image_le ?_ + simp + /-- A coordinate of a positive-arity relation has nonempty support. -/ theorem RelCoord.support_nonempty (c : RelCoord S V) (h : 0 < S.arity c.1) : c.support.Nonempty := by diff --git a/Graphon/RelIidEdgeRegression.lean b/Graphon/RelIidEdgeRegression.lean index 2cb3fd2..98ca8dd 100644 --- a/Graphon/RelIidEdgeRegression.lean +++ b/Graphon/RelIidEdgeRegression.lean @@ -347,6 +347,144 @@ theorem rankThreeCoupling_truncation : ← Measure.map_prod_map _ _ measurable_arr measurable_id, Measure.map_id, rankTwoCoupling, iidEdgeLaw] +/-! ### Blocks read a single edge coordinate + +Two pointwise lemmas, proved before any measure is touched: a block below rank two is constant +`false`, and a block at a two-point support reads exactly the edge coordinate keyed by that +support. Everything downstream — recovery at both ranks and screening at rank two — is a +consequence of these. -/ + +open scoped Classical in +/-- A block whose support does not have two elements is constant `false`. -/ +theorem blockMap_arr_of_card_ne_two {A : Finset (Σ _ : Unit, ℕ)} (hA : A.card ≠ 2) (e : Edges) : + blockMap (S := digraphSig) A (arr e) = fun _ => false := by + funext c + show arr e c.1 = false + rw [arr, dif_neg] + rw [c.2] + exact hA + +open scoped Classical in +/-- A block at a two-point support reads exactly the edge coordinate keyed by that support. -/ +theorem blockMap_arr_of_card_eq_two {A : Finset (Σ _ : Unit, ℕ)} (hA : A.card = 2) (e : Edges) : + blockMap (S := digraphSig) A (arr e) = + fun _ => decide (e (Subtype.mk A hA : RankSupport digraphSig 2) ≤ 1 / 2) := by + funext c + show arr e c.1 = _ + rw [arr, dif_pos (by rw [c.2]; exact hA)] + exact congrArg (fun r : ℝ => decide (r ≤ 1 / 2)) (congrArg e (Subtype.ext c.2)) + +/-! ### Rank-two invariance and recovery -/ + +/-- **Rank-two invariance**: the coupling is a product of two invariant factors. -/ +theorem rankTwoCoupling_invariant (σ : FinSuppPerm digraphSig) : + rankTwoCoupling.map (Prod.map (RelStructure.relabel σ.1) (⇑(rankLatentRelabel σ 2))) = + rankTwoCoupling := by + rw [rankTwoCoupling, ← Measure.map_prod_map _ _ (measurable_relabel σ.1) + (rankLatentRelabel σ 2).measurable, + iidEdgeLaw_map_relabel, rankLatentSource_map_rankLatentRelabel] + +open scoped Classical in +/-- **Rank-two local recovery**: below rank two every block is constant `false`, so the decoder +is a constant and reads no latent at all. -/ +theorem lower_recovers_rank_two (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card < 2) : + ∃ g : LocalLatentSpace (S := digraphSig) A 2 → BlockSpace (S := digraphSig) A, Measurable g ∧ + blockMap (S := digraphSig) A ∘ Prod.fst =ᵐ[rankTwoCoupling] + g ∘ localLatents (S := digraphSig) A 2 ∘ Prod.snd := by + refine ⟨fun _ _ => false, measurable_const, ?_⟩ + have hset : MeasurableSet {X : RelStructure digraphSig (Vinfinite digraphSig) | + blockMap (S := digraphSig) A X = fun _ => false} := + measurableSet_eq_fun (measurable_blockMap (S := digraphSig) A) measurable_const + refine (ae_map_iff measurable_fst.aemeasurable hset).mp ?_ + rw [rankTwoCoupling_map_fst, iidEdgeLaw] + refine (ae_map_iff measurable_arr.aemeasurable hset).mpr + (Filter.Eventually.of_forall fun e => ?_) + exact blockMap_arr_of_card_ne_two (by omega) e + +/-! ### Rank three: deterministic recovery and a vacuous screening clause + +At rank three recovery is the substantive clause — a two-point block is decoded from the latent +coordinate at its own support, which the rank-three array carries. Screening, by contrast, is +vacuous: over a binary signature no coordinate reads three vertices, so a three-point block space +is a single point. -/ + +/-- The fresh rank-two layer of a rank-three latent point reads the coordinate at that support. -/ +theorem freshLayer_apply (ω : RankLatentSpace digraphSig 3) (A : Finset (Σ _ : Unit, ℕ)) + (hA : A.card = 2) : + freshLayer ω (Subtype.mk A hA : RankSupport digraphSig 2) = + ω (Subtype.mk A (by omega) : RankLatentIndex digraphSig 3) := rfl + +open scoped Classical in +/-- **The rank-three decoder** at a two-point support: read the local latent at that very +support. -/ +noncomputable def twoPointDecoder (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card = 2) : + LocalLatentSpace (S := digraphSig) A 3 → BlockSpace (S := digraphSig) A := + fun ℓ _ => decide (ℓ ⟨Subtype.mk A (by omega), Finset.Subset.refl A⟩ ≤ 1 / 2) + +open scoped Classical in +theorem measurable_twoPointDecoder (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card = 2) : + Measurable (twoPointDecoder A hA) := + measurable_pi_lambda _ fun _ => measurable_decideLe (measurable_pi_apply _) + +open scoped Classical in +/-- **Rank-three local recovery**: below rank three a block is either constant `false` or, at a +two-point support, decoded from the latent coordinate at that support — which the rank-three +array carries, since `2 < 3`. This is the staging clause the regression exists to exercise. -/ +theorem lower_recovers_rank_three (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card < 3) : + ∃ g : LocalLatentSpace (S := digraphSig) A 3 → BlockSpace (S := digraphSig) A, Measurable g ∧ + blockMap (S := digraphSig) A ∘ Prod.fst =ᵐ[rankThreeCoupling] + g ∘ localLatents (S := digraphSig) A 3 ∘ Prod.snd := by + by_cases h2 : A.card = 2 + · refine ⟨twoPointDecoder A h2, measurable_twoPointDecoder A h2, ?_⟩ + rw [rankThreeCoupling] + refine (ae_map_iff measurable_rankThreeMap.aemeasurable ?_).mpr + (Filter.Eventually.of_forall fun ω => ?_) + · exact measurableSet_eq_fun ((measurable_blockMap (S := digraphSig) A).comp measurable_fst) + ((measurable_twoPointDecoder A h2).comp + ((measurable_localLatents (S := digraphSig) A 3).comp measurable_snd)) + · show blockMap (S := digraphSig) A (arr (freshLayer ω)) = _ + rw [blockMap_arr_of_card_eq_two h2, freshLayer_apply ω A h2] + rfl + · refine ⟨fun _ _ => false, measurable_const, ?_⟩ + rw [rankThreeCoupling] + refine (ae_map_iff measurable_rankThreeMap.aemeasurable ?_).mpr + (Filter.Eventually.of_forall fun ω => ?_) + · exact measurableSet_eq_fun ((measurable_blockMap (S := digraphSig) A).comp measurable_fst) + measurable_const + · exact blockMap_arr_of_card_ne_two h2 (freshLayer ω) + +/-- Over a binary signature a coordinate reads at most two vertices. -/ +theorem card_support_le_two (c : RelCoord digraphSig (Vinfinite digraphSig)) : + c.support.card ≤ 2 := RelCoord.card_support_le c + +open scoped Classical in +/-- **No coordinate has a three-point support**, so a rank-three block space is a single point — +which is why the rank-three screening clause carries no probabilistic content. -/ +theorem isEmpty_blockIndex_of_card_eq_three {A : Finset (Σ _ : Unit, ℕ)} (hA : A.card = 3) : + IsEmpty (BlockIndex (S := digraphSig) A) := + ⟨fun c => by + have := card_support_le_two c.1 + rw [c.2, hA] at this + omega⟩ + +open scoped Classical in +/-- **Rank-three screening**: at a three-point support the block space is a single point, so the +block is a constant and conditional independence is immediate. -/ +theorem screening_rank_three (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card = 3) : + CondIndepFun (MeasurableSpace.comap + (localLatents (S := digraphSig) A 3 ∘ Prod.snd) inferInstance) + (((measurable_localLatents (S := digraphSig) A 3).comp measurable_snd).comap_le) + (blockMap (S := digraphSig) A ∘ Prod.fst) (restObservation 3 A) rankThreeCoupling := by + haveI := isEmpty_blockIndex_of_card_eq_three hA + haveI : Unique (BlockSpace (S := digraphSig) A) := Pi.uniqueOfIsEmpty _ + have hconst : (blockMap (S := digraphSig) A ∘ Prod.fst : + RelStructure digraphSig (Vinfinite digraphSig) × RankLatentSpace digraphSig 3 → + BlockSpace (S := digraphSig) A) = fun _ => default := + funext fun _ => Subsingleton.elim _ _ + rw [hconst] + exact condIndepFun_const_left (default : BlockSpace (S := digraphSig) A) + (restObservation (S := digraphSig) 3 A) + end IidEdgeRegression end RelSignature From 8db367fd33cbec07d58523acc2c17550ad765f28 Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 19 Aug 2026 13:57:01 +0000 Subject: [PATCH 07/11] feat: rank-two screening, both representations, and the successor witness (#196) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rank-two screening is the clause this regression exists to exercise. At a two-point support the block reads **one** coordinate of the edge source, while the remainder reads the other coordinates plus the whole latent array — an independent factor. So the block is independent of the remainder outright, and screening follows from independence rather than from determinism. The bipartite regression could not test this: there the rank-two block was a function of the latents visible at its support, so screening was immediate. The private lemma is accordingly generalized from the two coordinates of a product to abstract σ-algebras: **if m₁ is independent of m₂, conditioning on anything inside m₂ cannot create a dependence.** The generalization is forced, not cosmetic — the ambient measure here is a pushforward of a product along the non-injective thresholding map, and conditional independence does not transport forward along such a map, whereas independence, being a property of a joint law, does. The repository has no forward transport for the conditional statement and this is why none is needed. The supporting split is `Equiv.sumCompl` at the distinguished support followed by `infinitePi_map_comp_equiv` and `infinitePi_map_sumPiEquivProdPi`, then `prodAssoc_prod` to put the single coordinate against everything else. With rank-three invariance from the joint pointwise action, both representations package and `iidEdgeSuccessor` witnesses the rank 2 → 3 step with exact truncation. --- Graphon/RelIidEdgeRegression.lean | 360 ++++++++++++++++++++++++------ 1 file changed, 294 insertions(+), 66 deletions(-) diff --git a/Graphon/RelIidEdgeRegression.lean b/Graphon/RelIidEdgeRegression.lean index 98ca8dd..75c4d8a 100644 --- a/Graphon/RelIidEdgeRegression.lean +++ b/Graphon/RelIidEdgeRegression.lean @@ -174,82 +174,58 @@ noncomputable def iidEdgeExchangeable : InfiniteRelExchangeableLaw digraphSig wh law := ⟨iidEdgeLaw, inferInstance⟩ exchangeable := iidEdgeLaw_map_relabel -/-! ### The product-right conditional-independence lemma +/-! ### Conditional independence from unconditional independence Kept **private**: it has one consumer (rank-two screening below), which is below the promotion bar for `Graphon/ForMathlib/`. Neither Mathlib nor TauCeti has it — `condExp_indep_eq` supplies the -constant conditional expectation of a left-coordinate observation, but not the intersection -identity that conditional independence needs. Recorded as a prospective upstream candidate. - -Stated for an arbitrary conditioning σ-algebra below `comap Prod.snd`, so conditioning on a -function of the right coordinate is a corollary rather than the definition. - -Two elaboration points are load-bearing. `CondIndepFun` takes the conditioning algebra *before* the -ambient measurable space, so the conclusion is written in explicit `@` form. And an abstract -`m' : MeasurableSpace (α × β)` binder **enters local instance search**, shadowing the product -instance throughout the proof body; the opening `letI` restores the intended ambient instance -without weakening the statement. -/ - -private theorem comap_fst_le_prod {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : - MeasurableSpace.comap (Prod.fst : α × β → α) inferInstance ≤ - (Prod.instMeasurableSpace : MeasurableSpace (α × β)) := by - rintro S ⟨T, hT, rfl⟩ - exact measurable_fst hT - -private theorem comap_snd_le_prod {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : - MeasurableSpace.comap (Prod.snd : α × β → β) inferInstance ≤ - (Prod.instMeasurableSpace : MeasurableSpace (α × β)) := by - rintro S ⟨T, hT, rfl⟩ - exact measurable_snd hT - -open scoped Classical in -/-- Under a product measure, a left-coordinate observation is conditionally independent of a -right-coordinate observation given **any** σ-algebra below the right coordinate's. -/ -private theorem condIndepFun_of_prod_right {α β γ δ : Type*} - [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] - [StandardBorelSpace α] [StandardBorelSpace β] [Nonempty α] [Nonempty β] - {μ : Measure α} {ν : Measure β} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] - {m' : MeasurableSpace (α × β)} - (hm' : m' ≤ MeasurableSpace.comap (Prod.snd : α × β → β) inferInstance) - {f : α → γ} {g : β → δ} (hf : Measurable f) (hg : Measurable g) : - @ProbabilityTheory.CondIndepFun (α × β) m' Prod.instMeasurableSpace - (StandardBorelSpace.prod) (hm'.trans comap_snd_le_prod) - γ δ inferInstance inferInstance - (f ∘ (Prod.fst : α × β → α)) (g ∘ (Prod.snd : α × β → β)) (μ.prod ν) inferInstance := by - letI mΩ : MeasurableSpace (α × β) := Prod.instMeasurableSpace - have hmAmbient : m' ≤ (Prod.instMeasurableSpace : MeasurableSpace (α × β)) := - hm'.trans comap_snd_le_prod - have hfst : Measurable (f ∘ (Prod.fst : α × β → α)) := hf.comp measurable_fst - have hsnd : Measurable (g ∘ (Prod.snd : α × β → β)) := hg.comp measurable_snd - have hcoord : Indep (MeasurableSpace.comap (Prod.fst : α × β → α) inferInstance) - (MeasurableSpace.comap (Prod.snd : α × β → β) inferInstance) (μ.prod ν) := - indepFun_prod measurable_id measurable_id - rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hfst hsnd] +constant conditional expectation of an `m₁`-observation, but not the intersection identity that +conditional independence needs. Recorded as a prospective upstream candidate. + +**If `m₁` is independent of `m₂`, then conditioning on anything inside `m₂` cannot create a +dependence.** Stated for abstract σ-algebras rather than for the two coordinates of a product, +because the consumer's ambient measure is a *pushforward* of a product and only the independence +survives that pushforward — conditional independence does not transport forward along a +non-injective map. + +One elaboration point is load-bearing: an abstract `MeasurableSpace Ω` binder **enters local +instance search** and can shadow the ambient instance throughout the proof body. The conclusion is +therefore written in explicit `@` form and the proof opens with a `letI` restoring the intended +ambient instance, neither of which weakens the statement. -/ + +private theorem condIndepFun_of_indep_of_le {Ω γ δ : Type*} [mΩ : MeasurableSpace Ω] + [hsb : StandardBorelSpace Ω] [MeasurableSpace γ] [MeasurableSpace δ] + {μ : Measure Ω} [IsProbabilityMeasure μ] + {m' m₁ m₂ : MeasurableSpace Ω} (h1 : m₁ ≤ mΩ) (h2 : m₂ ≤ mΩ) (hm' : m' ≤ m₂) + (hindep : Indep m₁ m₂ μ) {f : Ω → γ} {g : Ω → δ} + (hf : Measurable[m₁] f) (hg : Measurable[m₂] g) : + @ProbabilityTheory.CondIndepFun Ω m' mΩ hsb (hm'.trans h2) γ δ inferInstance inferInstance + f g μ inferInstance := by + letI : MeasurableSpace Ω := mΩ + have hmAmbient : m' ≤ mΩ := hm'.trans h2 + have hfm : Measurable f := hf.mono h1 le_rfl + have hgm : Measurable g := hg.mono h2 le_rfl + rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hfm hgm] intro s t hs ht - set A : Set (α × β) := (f ∘ (Prod.fst : α × β → α)) ⁻¹' s with hAdef - set B : Set (α × β) := (g ∘ (Prod.snd : α × β → β)) ⁻¹' t with hBdef - have hAmem : MeasurableSet[MeasurableSpace.comap (Prod.fst : α × β → α) inferInstance] A := - ⟨f ⁻¹' s, hf hs, rfl⟩ - have hBmem : MeasurableSet[MeasurableSpace.comap (Prod.snd : α × β → β) inferInstance] B := - ⟨g ⁻¹' t, hg ht, rfl⟩ - have hAmeas : MeasurableSet A := hfst hs - have hBmeas : MeasurableSet B := hsnd ht - have hAconst : (μ.prod ν)⟦A | m'⟧ =ᵐ[μ.prod ν] fun _ => ((μ.prod ν) A).toReal := by - have hInd : Indep (MeasurableSpace.comap (Prod.fst : α × β → α) inferInstance) m' - (μ.prod ν) := indep_of_indep_of_le_right hcoord hm' - refine (condExp_indep_eq (μ := μ.prod ν) comap_fst_le_prod hmAmbient + set A : Set Ω := f ⁻¹' s with hAdef + set B : Set Ω := g ⁻¹' t with hBdef + have hAmem : MeasurableSet[m₁] A := hf hs + have hBmem : MeasurableSet[m₂] B := hg ht + have hAmeas : MeasurableSet A := hfm hs + have hBmeas : MeasurableSet B := hgm ht + have hAconst : μ⟦A | m'⟧ =ᵐ[μ] fun _ => (μ A).toReal := by + have hInd : Indep m₁ m' μ := indep_of_indep_of_le_right hindep hm' + refine (condExp_indep_eq (μ := μ) h1 hmAmbient (stronglyMeasurable_const.indicator hAmem) hInd).trans (Filter.Eventually.of_forall fun _ => ?_) rw [integral_indicator_const (1 : ℝ) hAmeas, smul_eq_mul, mul_one, measureReal_def] - have hInter : (μ.prod ν)⟦A ∩ B | m'⟧ =ᵐ[μ.prod ν] - fun ω => ((μ.prod ν) A).toReal * ((μ.prod ν)⟦B | m'⟧) ω := by + have hInter : μ⟦A ∩ B | m'⟧ =ᵐ[μ] fun ω => (μ A).toReal * (μ⟦B | m'⟧) ω := by refine (ae_eq_condExp_of_forall_setIntegral_eq hmAmbient ((integrable_const (1 : ℝ)).indicator (hAmeas.inter hBmeas)) (fun S _ _ => (integrable_condExp.const_mul _).integrableOn) (fun S hSm _ => ?_) (stronglyMeasurable_condExp.const_mul _).aestronglyMeasurable).symm have hSamb : MeasurableSet S := hmAmbient _ hSm - have hmul : (μ.prod ν) (A ∩ (S ∩ B)) = (μ.prod ν) A * (μ.prod ν) (S ∩ B) := by - simpa using hcoord A (S ∩ B) hAmem ((hm' _ hSm).inter hBmem) + have hmul : μ (A ∩ (S ∩ B)) = μ A * μ (S ∩ B) := by + simpa using hindep A (S ∩ B) hAmem ((hm' _ hSm).inter hBmem) rw [integral_const_mul, setIntegral_condExp hmAmbient ((integrable_const (1 : ℝ)).indicator hBmeas) hSm, setIntegral_indicator hBmeas, setIntegral_indicator (hAmeas.inter hBmeas), @@ -258,8 +234,8 @@ private theorem condIndepFun_of_prod_right {α β γ δ : Type*} show S ∩ (A ∩ B) = A ∩ (S ∩ B) from Set.inter_left_comm _ _ _, measureReal_def, measureReal_def, hmul, ENNReal.toReal_mul] ring - filter_upwards [hInter, hAconst] with ω h1 h2 - rw [h1, h2] + filter_upwards [hInter, hAconst] with ω hi ha + rw [hi, ha] /-! ### The two couplings, described independently @@ -485,6 +461,258 @@ theorem screening_rank_three (A : Finset (Σ _ : Unit, ℕ)) (hA : A.card = 3) : exact condIndepFun_const_left (default : BlockSpace (S := digraphSig) A) (restObservation (S := digraphSig) 3 A) +/-! ### Rank-two screening + +At a two-point support the block reads **one** coordinate of the edge source, while the remainder +reads the *other* coordinates together with the whole latent array — an independent factor. So the +block is independent of the remainder outright, and screening follows from independence rather than +from determinism. That is the case the bipartite regression could not exercise: there the rank-two +block was a function of the latents visible at its support, so screening was immediate. + +Independence, unlike conditional independence, is a property of a joint law and therefore survives +the pushforward along the (non-injective) thresholding map that builds the structure. The argument +accordingly establishes the unconditional independence on the source and transports *that*. -/ + +private theorem indepFun_of_map {Ω Ω' γ δ : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω'] + [MeasurableSpace γ] [MeasurableSpace δ] {μ : Measure Ω} [IsProbabilityMeasure μ] + {T : Ω → Ω'} (hT : Measurable T) {f : Ω' → γ} {g : Ω' → δ} + (hf : Measurable f) (hg : Measurable g) (h : IndepFun (f ∘ T) (g ∘ T) μ) : + IndepFun f g (μ.map T) := by + haveI : IsProbabilityMeasure (μ.map T) := Measure.isProbabilityMeasure_map hT.aemeasurable + rw [indepFun_iff_map_prod_eq_prod_map_map hf.aemeasurable hg.aemeasurable, + Measure.map_map (hf.prodMk hg) hT, Measure.map_map hf hT, Measure.map_map hg hT] + exact (indepFun_iff_map_prod_eq_prod_map_map (hf.comp hT).aemeasurable + (hg.comp hT).aemeasurable).mp h + +/-- The edge coordinate at the distinguished support. -/ +private abbrev AtIdx (A₀ : RankSupport digraphSig 2) := {x : RankSupport digraphSig 2 // x = A₀} + +/-- The edge coordinates away from the distinguished support. -/ +private abbrev OffIdx (A₀ : RankSupport digraphSig 2) := + {x : RankSupport digraphSig 2 // ¬(x = A₀)} + +open scoped Classical in +/-- **Splitting the edge source at one coordinate.** -/ +private theorem iidUniformSource_split (A₀ : RankSupport digraphSig 2) : + (iidUniformSource (RankSupport digraphSig 2)).map + (fun u : Edges => ((fun B : AtIdx A₀ => u B.1), (fun B : OffIdx A₀ => u B.1))) = + (iidUniformSource (AtIdx A₀)).prod (iidUniformSource (OffIdx A₀)) := by + have hpre : Measurable fun (u : Edges) (i : AtIdx A₀ ⊕ OffIdx A₀) => + u (Equiv.sumCompl (fun x : RankSupport digraphSig 2 => x = A₀) i) := + measurable_pi_lambda _ fun _ => measurable_pi_apply _ + rw [show (fun u : Edges => ((fun B : AtIdx A₀ => u B.1), (fun B : OffIdx A₀ => u B.1))) = + ⇑(MeasurableEquiv.sumPiEquivProdPi fun _ : AtIdx A₀ ⊕ OffIdx A₀ => ℝ) ∘ + (fun (u : Edges) (i : AtIdx A₀ ⊕ OffIdx A₀) => + u (Equiv.sumCompl (fun x : RankSupport digraphSig 2 => x = A₀) i)) from rfl, + ← Measure.map_map (MeasurableEquiv.sumPiEquivProdPi + fun _ : AtIdx A₀ ⊕ OffIdx A₀ => ℝ).measurable hpre, + iidUniformSource, + Measure.infinitePi_map_comp_equiv _ + (Equiv.sumCompl (fun x : RankSupport digraphSig 2 => x = A₀)), + Measure.infinitePi_map_sumPiEquivProdPi] + rfl + +/-- The source observation: the distinguished edge coordinate, against everything else. -/ +private def srcObs (A₀ : RankSupport digraphSig 2) : + Edges × RankLatentSpace digraphSig 2 → + (AtIdx A₀ → ℝ) × ((OffIdx A₀ → ℝ) × RankLatentSpace digraphSig 2) := + fun p => ((fun B => p.1 B.1), ((fun B => p.1 B.1), p.2)) + +private theorem measurable_srcObs (A₀ : RankSupport digraphSig 2) : Measurable (srcObs A₀) := + ((measurable_pi_lambda _ fun _ => measurable_fst.eval)).prodMk + ((measurable_pi_lambda _ fun _ => measurable_fst.eval).prodMk measurable_snd) + +private theorem map_srcObs (A₀ : RankSupport digraphSig 2) : + ((iidUniformSource (RankSupport digraphSig 2)).prod + (rankLatentSource digraphSig 2)).map (srcObs A₀) = + (iidUniformSource (AtIdx A₀)).prod + ((iidUniformSource (OffIdx A₀)).prod (rankLatentSource digraphSig 2)) := by + have hsplit : Measurable + (fun u : Edges => ((fun B : AtIdx A₀ => u B.1), (fun B : OffIdx A₀ => u B.1))) := + (measurable_pi_lambda _ fun _ => measurable_pi_apply _).prodMk + (measurable_pi_lambda _ fun _ => measurable_pi_apply _) + rw [show srcObs A₀ = ⇑(MeasurableEquiv.prodAssoc) ∘ + Prod.map (fun u : Edges => ((fun B : AtIdx A₀ => u B.1), (fun B : OffIdx A₀ => u B.1))) + (id : RankLatentSpace digraphSig 2 → _) from rfl, + ← Measure.map_map (MeasurableEquiv.prodAssoc).measurable (hsplit.prodMap measurable_id), + ← Measure.map_prod_map _ _ hsplit measurable_id, iidUniformSource_split, Measure.map_id, + Measure.prodAssoc_prod] + +private theorem indepFun_srcObs (A₀ : RankSupport digraphSig 2) : + IndepFun (fun p => (srcObs A₀ p).1) (fun p => (srcObs A₀ p).2) + ((iidUniformSource (RankSupport digraphSig 2)).prod (rankLatentSource digraphSig 2)) := by + rw [indepFun_iff_map_prod_eq_prod_map_map (measurable_srcObs A₀).fst.aemeasurable + (measurable_srcObs A₀).snd.aemeasurable, + show (fun p => ((srcObs A₀ p).1, (srcObs A₀ p).2)) = srcObs A₀ from rfl, + show (fun p => (srcObs A₀ p).1) = Prod.fst ∘ srcObs A₀ from rfl, + show (fun p => (srcObs A₀ p).2) = Prod.snd ∘ srcObs A₀ from rfl, + ← Measure.map_map measurable_fst (measurable_srcObs A₀), + ← Measure.map_map measurable_snd (measurable_srcObs A₀), + map_srcObs A₀, Measure.map_fst_prod, Measure.map_snd_prod] + simp + +open scoped Classical in +/-- The block at the distinguished support, read off its own edge coordinate. -/ +private noncomputable def blockDecoder (A₀ : RankSupport digraphSig 2) : + (AtIdx A₀ → ℝ) → BlockSpace (S := digraphSig) A₀.1 := + fun t _ => decide (t ⟨A₀, rfl⟩ ≤ 1 / 2) + +open scoped Classical in +private theorem measurable_blockDecoder (A₀ : RankSupport digraphSig 2) : + Measurable (blockDecoder A₀) := + measurable_pi_lambda _ fun _ => measurable_decideLe (measurable_pi_apply _) + +open scoped Classical in +/-- The remainder, read off the other edge coordinates and the latent array. -/ +private noncomputable def restDecoder (A₀ : RankSupport digraphSig 2) : + (OffIdx A₀ → ℝ) × RankLatentSpace digraphSig 2 → + RestSpace (S := digraphSig) 2 A₀.1 × RankLatentSpace digraphSig 2 := + fun q => (fun c => if h : c.1.support.card = 2 then + decide (q.1 ⟨⟨c.1.support, h⟩, fun hEq => c.2.2 (congrArg Subtype.val hEq)⟩ ≤ 1 / 2) + else false, q.2) + +open scoped Classical in +private theorem measurable_restDecoder (A₀ : RankSupport digraphSig 2) : + Measurable (restDecoder A₀) := by + refine (measurable_pi_lambda _ fun c => ?_).prodMk measurable_snd + by_cases h : c.1.support.card = 2 + · simp only [dif_pos h] + exact measurable_decideLe measurable_fst.eval + · simp only [dif_neg h] + exact measurable_const + +open scoped Classical in +private theorem block_comp (A₀ : RankSupport digraphSig 2) : + (blockMap (S := digraphSig) A₀.1 ∘ Prod.fst) ∘ + Prod.map arr (id : RankLatentSpace digraphSig 2 → _) = + blockDecoder A₀ ∘ fun p => (srcObs A₀ p).1 := by + funext p + show blockMap (S := digraphSig) A₀.1 (arr p.1) = _ + rw [blockMap_arr_of_card_eq_two A₀.2] + rfl + +open scoped Classical in +private theorem rest_comp (A₀ : RankSupport digraphSig 2) : + restObservation (S := digraphSig) 2 A₀.1 ∘ + Prod.map arr (id : RankLatentSpace digraphSig 2 → _) = + restDecoder A₀ ∘ fun p => (srcObs A₀ p).2 := by + funext p + refine Prod.ext ?_ rfl + funext c + rfl + +open scoped Classical in +/-- **The block is independent of the remainder**: they read disjoint edge coordinates, and the +latent array is an independent factor. -/ +private theorem indepFun_block_rest (A₀ : RankSupport digraphSig 2) : + IndepFun (blockMap (S := digraphSig) A₀.1 ∘ Prod.fst) + (restObservation (S := digraphSig) 2 A₀.1) rankTwoCoupling := by + have hcoupling : rankTwoCoupling = + ((iidUniformSource (RankSupport digraphSig 2)).prod + (rankLatentSource digraphSig 2)).map + (Prod.map arr (id : RankLatentSpace digraphSig 2 → _)) := by + rw [rankTwoCoupling, iidEdgeLaw, ← Measure.map_prod_map _ _ measurable_arr measurable_id, + Measure.map_id] + rw [hcoupling] + refine indepFun_of_map (measurable_arr.prodMap measurable_id) + ((measurable_blockMap (S := digraphSig) A₀.1).comp measurable_fst) + (measurable_restObservation 2 A₀.1) ?_ + rw [block_comp A₀, rest_comp A₀] + exact (indepFun_srcObs A₀).comp (measurable_blockDecoder A₀) (measurable_restDecoder A₀) + +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 independent of that +remainder outright, and the conditioning algebra sits inside the remainder's. -/ +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 + have hm' : MeasurableSpace.comap + (localLatents (S := digraphSig) A 2 ∘ Prod.snd) inferInstance ≤ + MeasurableSpace.comap (restObservation (S := digraphSig) 2 A) inferInstance := by + rw [show (localLatents (S := digraphSig) A 2 ∘ Prod.snd) = + (localLatents (S := digraphSig) A 2 ∘ Prod.snd) ∘ + restObservation (S := digraphSig) 2 A from rfl, + ← MeasurableSpace.comap_comp] + exact MeasurableSpace.comap_mono + ((measurable_localLatents (S := digraphSig) A 2).comp measurable_snd).comap_le + exact condIndepFun_of_indep_of_le + ((measurable_blockMap (S := digraphSig) A).comp measurable_fst).comap_le + (measurable_restObservation (S := digraphSig) 2 A).comap_le hm' + ((IndepFun_iff_Indep _ _ _).mp (indepFun_block_rest (⟨A, hA⟩ : RankSupport digraphSig 2))) + (comap_measurable _) (comap_measurable _) + +/-! ### Rank-three invariance, the two representations, and the successor witness -/ + +open scoped Classical in +/-- The fresh layer intertwines the rank-three latent action with the vertex action. -/ +theorem freshLayer_rankLatentRelabel (σ : FinSuppPerm digraphSig) + (ω : RankLatentSpace digraphSig 3) : + freshLayer (rankLatentRelabel σ 3 ω) = fun A => freshLayer ω (rankSupportPerm σ.1 2 A) := by + funext A + show (rankLatentSpaceSuccEquiv 2 (rankLatentRelabel σ 3 ω)).2 A = _ + rw [show rankLatentSpaceSuccEquiv 2 (rankLatentRelabel σ 3 ω) = + MeasurableEquiv.prodCongr (rankLatentRelabel σ 2) (rankSupportLatentRelabel σ 2) + (rankLatentSpaceSuccEquiv 2 ω) from + congrFun (rankLatentSpaceSuccEquiv_rankLatentRelabel σ 2) ω] + rfl + +open scoped Classical in +/-- **The exact pointwise joint action** at rank three. -/ +theorem jointMap_rankLatentRelabel (σ : FinSuppPerm digraphSig) + (ω : RankLatentSpace digraphSig 3) : + (arr (freshLayer (rankLatentRelabel σ 3 ω)), rankLatentRelabel σ 3 ω) = + Prod.map (RelStructure.relabel σ.1) (⇑(rankLatentRelabel σ 3)) + (arr (freshLayer ω), ω) := by + refine Prod.ext ?_ rfl + show arr (freshLayer (rankLatentRelabel σ 3 ω)) = RelStructure.relabel σ.1 (arr (freshLayer ω)) + rw [freshLayer_rankLatentRelabel, arr_comp_supportPerm] + +/-- **Rank-three invariance**: the joint action, then source invariance. -/ +theorem rankThreeCoupling_invariant (σ : FinSuppPerm digraphSig) : + rankThreeCoupling.map (Prod.map (RelStructure.relabel σ.1) (⇑(rankLatentRelabel σ 3))) = + rankThreeCoupling := by + rw [rankThreeCoupling, Measure.map_map + ((measurable_relabel σ.1).prodMap (rankLatentRelabel σ 3).measurable) + measurable_rankThreeMap, + show (Prod.map (RelStructure.relabel σ.1) (⇑(rankLatentRelabel σ 3)) ∘ + fun ω : RankLatentSpace digraphSig 3 => (arr (freshLayer ω), ω)) = + (fun ω : RankLatentSpace digraphSig 3 => (arr (freshLayer ω), ω)) ∘ + (rankLatentRelabel σ 3) from by + funext ω + exact (jointMap_rankLatentRelabel σ ω).symm, + ← Measure.map_map measurable_rankThreeMap (rankLatentRelabel σ 3).measurable, + rankLatentSource_map_rankLatentRelabel] + +/-- **The rank-two representation** of the i.i.d.-edge law. -/ +noncomputable def rankTwoRep : iidEdgeExchangeable.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 rank-three representation** of the same law. -/ +noncomputable def rankThreeRep : iidEdgeExchangeable.RankRepresentation 3 where + P := rankThreeCoupling + isProbabilityMeasure_P := inferInstance + map_fst := rankThreeCoupling_map_fst + map_snd := rankThreeCoupling_map_snd + invariant := rankThreeCoupling_invariant + lower_recovers := lower_recovers_rank_three + screening := screening_rank_three + +/-- **The successor witness**: the rank-three representation truncates back to the +*independently defined* rank-two one, on the nose. -/ +noncomputable def iidEdgeSuccessor : + InfiniteRelExchangeableLaw.RankSuccessor rankTwoRep where + next := rankThreeRep + truncation := rankThreeCoupling_truncation + end IidEdgeRegression end RelSignature From 86046417d7d2fa6c1828880f4299e9f5b11e47ba Mon Sep 17 00:00:00 2001 From: Cameron Freer Date: Wed, 19 Aug 2026 14:07:56 +0000 Subject: [PATCH 08/11] feat: nondegeneracy, decoding identity, and wiring for the i.i.d.-edge regression (#196) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly one half, so no block is almost surely constant and rank-two screening is a genuine conditional- independence statement rather than determinism in disguise — the numerical counterpart of the bipartite regression's 1/2-vs-1/4 check. `ae_edge_eq_decode` states the staging property concretely: under the rank-three coupling the edge at a two-point support is the thresholded latent coordinate keyed by that support. Module wired into `Graphon.lean` with its index entry; audit 415 → 424 in both `scripts/axiom_audit.lean` and the intended-set literal in `scripts/check_census_and_axioms.py` (counted directly). Gates: lake build clean (3407 jobs), census + axiom audit pass, zero sorries. --- Graphon.lean | 2 + Graphon/RelIidEdgeRegression.lean | 94 +++++++++++++++++++++++++++++- scripts/axiom_audit.lean | 11 ++++ scripts/check_census_and_axioms.py | 9 +++ 4 files changed, 114 insertions(+), 2 deletions(-) diff --git a/Graphon.lean b/Graphon.lean index 4ed861c..e881bac 100644 --- a/Graphon.lean +++ b/Graphon.lean @@ -50,6 +50,7 @@ import Graphon.RelPooledExtension import Graphon.RelPooledAcceptance import Graphon.RelRankSuccessorContract import Graphon.RelBipartiteRegression +import Graphon.RelIidEdgeRegression import Graphon.RelSingletonPeel import Graphon.RelFixingAlgebra import Graphon.RelRankAlgebra @@ -271,6 +272,7 @@ in Lean 4 using Mathlib. * `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_{