From 61d7f62beffb51d877a9b43a00ac9dddd3042fad Mon Sep 17 00:00:00 2001
From: Cameron Freer <freer@mit.edu>
Date: Thu, 30 Jul 2026 19:25:35 +0000
Subject: [PATCH 1/4] feat: the lower-rank factor of a coherent basis (#107)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Steps 2–3 of the lower-factor PR: the definitions, instances, and the measurability
half of the generation statement.

* `LowerIndex n = {i // (B.anchor i).card < n}`, countable, and **empty at `n = 0`**;
* `LowerFactorSpace n = LowerIndex n → Bool`, standard Borel since the index is
  countable, and a subsingleton at `n = 0`;
* `lowerFactorMap n X i = decide (X ∈ B.event i.1)`;
* `measurable_lowerFactorMap` for `lowerRankAlgebra n`, each coordinate being the
  indicator of an event whose anchor has rank `< n`, and `measurable_lowerFactorMap'`
  for the ambient σ-algebra;
* `comap_lowerFactorMap_le : comap (lowerFactorMap n) inferInstance ≤ lowerRankAlgebra n`
  — one half of the generation statement. **No raw equality**; the converse is eventwise
  and modulo the law, and comes later in this PR.

The module docstring records why the factor, and not the latents, carries the
conditioning: a latent normally holds randomness beyond the factor it represents
(`1_{U < p}` already generates strictly less than `U`), so a latent-generated σ-algebra
is typically strictly larger. It also records that `LowerIndex n` is deliberately *not*
Boolean-closed — two small anchors can combine to a large one — which is not a defect,
since the product σ-algebra still contains Boolean combinations of the coordinates.

No coupling, no augmented space, no `ξ∅`: those belong to the induction layer, which
should consume a settled lower-factor API rather than be mixed with it. No `NoNullary`.

Audit measured directly on base and head rather than carried: 210 → 213. Full build
3362 jobs green; census, axiom audit, and documentation drift checks pass.

Still to come in this PR: rank nesting with the `rfl` projection laws, finitary
relabeling equivariance at `FinSuppPerm`, the eventwise mod-null generation theorem, and
the rank-zero/rank-one regressions.
---
 Graphon.lean                       |   1 +
 Graphon/RelLowerFactor.lean        | 104 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean           |   3 +
 scripts/check_census_and_axioms.py |   3 +
 4 files changed, 111 insertions(+)
 create mode 100644 Graphon/RelLowerFactor.lean

diff --git a/Graphon.lean b/Graphon.lean
index 86e297b..5a41d02 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -23,6 +23,7 @@ import Graphon.RelKernelSampler
 import Graphon.KernelRandomization
 import Graphon.RelFixingAlgebra
 import Graphon.RelRankAlgebra
+import Graphon.RelLowerFactor
 import Graphon.RelPollingInfrastructure
 import Graphon.RelFixingCondIndep
 import Graphon.SeparableFactor
diff --git a/Graphon/RelLowerFactor.lean b/Graphon/RelLowerFactor.lean
new file mode 100644
index 0000000..5f88522
--- /dev/null
+++ b/Graphon/RelLowerFactor.lean
@@ -0,0 +1,104 @@
+/-
+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.RelCoherentBasis
+import Graphon.RelRankAlgebra
+
+/-!
+# The lower-rank factor of a coherent basis (R4 converse piece 3, #107)
+
+The factor coordinates whose anchors have cardinality below `n`: the structural object the
+rank induction conditions on.
+
+## Why the factor, not the latents
+
+The conditioning factor must be described by the *basis coordinates*, not by the latents that
+will eventually encode them. A latent normally carries randomness beyond the factor it
+represents — already `1_{U < p}` generates strictly less than `U` — so a σ-algebra generated by
+latents is typically strictly larger than the factor. Everything here is therefore stated about
+`lowerFactorMap`, and the coupling to latents is deliberately absent: it belongs to the
+augmented-induction layer, which should consume a settled lower-factor API rather than be mixed
+with it.
+
+## The generation statement
+
+Only
+
+`comap (lowerFactorMap n) inferInstance ≤ lowerRankAlgebra n`
+
+together with an eventwise mod-null converse. **No raw equality of measurable spaces** — the
+same discipline as everywhere else in this layer, and for the same reason.
+
+`LowerIndex n` is not closed under the Boolean operations: two small anchors can combine to a
+large one. That is not a defect and no closure should be engineered — the product σ-algebra on
+`LowerFactorSpace n` still contains Boolean combinations of the coordinates.
+-/
+
+open MeasureTheory MeasurableSpace
+
+namespace RelSignature
+
+namespace CoherentBasis
+
+universe u
+
+variable {S : RelSignature.{u}} {M : InfiniteRelExchangeableLaw S} (B : CoherentBasis M)
+
+/-! ### The lower-rank index and factor space -/
+
+/-- **The indices of rank below `n`**: basis coordinates whose anchor has cardinality `< n`. -/
+def LowerIndex (n : ℕ) := {i : B.ι // (B.anchor i).card < n}
+
+instance (n : ℕ) : Countable (B.LowerIndex n) := Subtype.countable
+
+/-- At rank bound `0` there are no such indices. -/
+instance : IsEmpty (B.LowerIndex 0) := ⟨fun i => absurd i.2 (by omega)⟩
+
+/-- **The lower-rank factor space**, standard Borel since the index is countable. -/
+abbrev LowerFactorSpace (n : ℕ) := B.LowerIndex n → Bool
+
+instance (n : ℕ) : StandardBorelSpace (B.LowerFactorSpace n) := inferInstance
+
+/-- At rank bound `0` the factor space is a single point. -/
+instance : Subsingleton (B.LowerFactorSpace 0) :=
+  ⟨fun _ _ => funext fun i => (IsEmpty.false i).elim⟩
+
+open scoped Classical in
+/-- **The lower-rank factor map**: evaluate every basis event anchored below rank `n`. -/
+noncomputable def lowerFactorMap (n : ℕ) :
+    RelStructure S (Vinfinite S) → B.LowerFactorSpace n :=
+  fun X i => decide (X ∈ B.event i.1)
+
+/-! ### Measurability -/
+
+open scoped Classical in
+/-- The lower-rank factor map is measurable for `lowerRankAlgebra n`: each coordinate is the
+indicator of an event whose anchor has rank `< n`. -/
+theorem measurable_lowerFactorMap (n : ℕ) :
+    Measurable[RelStructure.lowerRankAlgebra (S := S) n] (B.lowerFactorMap n) := by
+  classical
+  letI : MeasurableSpace (RelStructure S (Vinfinite S)) :=
+    RelStructure.lowerRankAlgebra (S := S) n
+  refine measurable_pi_iff.mpr fun i => measurable_to_bool ?_
+  have hmem : MeasurableSet[RelStructure.lowerRankAlgebra (S := S) n] (B.event i.1) :=
+    RelStructure.fixingAlgebra_le_lowerRankAlgebra i.2 _ (B.event_mem i.1)
+  convert hmem using 1
+  ext X
+  simp [lowerFactorMap]
+
+/-- **The pullback lands inside the conditioning factor.** This is one half of the generation
+statement; the converse is eventwise and modulo the law. -/
+theorem comap_lowerFactorMap_le (n : ℕ) :
+    MeasurableSpace.comap (B.lowerFactorMap n) inferInstance ≤
+      RelStructure.lowerRankAlgebra (S := S) n :=
+  (B.measurable_lowerFactorMap n).comap_le
+
+/-- The lower-rank factor map is measurable for the ambient σ-algebra too. -/
+theorem measurable_lowerFactorMap' (n : ℕ) : Measurable (B.lowerFactorMap n) :=
+  (B.measurable_lowerFactorMap n).mono (RelStructure.lowerRankAlgebra_le n) le_rfl
+
+end CoherentBasis
+
+end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 72d0f25..6fbb9d6 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -213,3 +213,6 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.RelStructure.lowerRankAlgebra_one
 #print axioms RelSignature.RelStructure.comap_relabel_lowerRankAlgebra
 #print axioms RelSignature.card_inter_lt_of_ne
+#print axioms RelSignature.CoherentBasis.measurable_lowerFactorMap
+#print axioms RelSignature.CoherentBasis.comap_lowerFactorMap_le
+#print axioms RelSignature.CoherentBasis.measurable_lowerFactorMap'
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 9117982..79b60e8 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -196,6 +196,9 @@
     "RelSignature.RelStructure.lowerRankAlgebra_one",
     "RelSignature.RelStructure.comap_relabel_lowerRankAlgebra",
     "RelSignature.card_inter_lt_of_ne",
+    "RelSignature.CoherentBasis.measurable_lowerFactorMap",
+    "RelSignature.CoherentBasis.comap_lowerFactorMap_le",
+    "RelSignature.CoherentBasis.measurable_lowerFactorMap'",
     "RelSignature.condExp_ae_eq_condExp_of_comap_eq",
     "RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel",
     "RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra",

From f84894b83056193b1f03f22df07bd6b0ef25532c Mon Sep 17 00:00:00 2001
From: Cameron Freer <freer@mit.edu>
Date: Fri, 31 Jul 2026 01:52:15 +0000
Subject: [PATCH 2/4] feat: cond-indep layer 3, lower-factor nesting +
 finite-factor projection (#107)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Rank nesting for the lower-rank factor and the single-support restriction
that the generation argument runs through.

* `lowerIndexEmbedding` / `lowerFactorProjection` for `n ≤ m`, with the
  projection-map compatibility and the cocycle law both definitional.
* `basisIndexToLowerIndex` / `lowerToFactorProjection`: coordinates anchored
  inside a support `A` of rank `< n` are coordinates of rank `< n`, so the
  lower-rank factor restricts to `FactorSpace A`, and that restriction
  composed with `lowerFactorMap n` is `factorMap A` by `rfl`.

This is the device that lets generation be settled support by support
rather than through the `iSup`.

Audit 213 -> 218.
---
 Graphon/RelLowerFactor.lean        | 51 ++++++++++++++++++++++++++++++
 scripts/axiom_audit.lean           |  5 +++
 scripts/check_census_and_axioms.py |  5 +++
 3 files changed, 61 insertions(+)

diff --git a/Graphon/RelLowerFactor.lean b/Graphon/RelLowerFactor.lean
index 5f88522..c88796c 100644
--- a/Graphon/RelLowerFactor.lean
+++ b/Graphon/RelLowerFactor.lean
@@ -99,6 +99,57 @@ theorem comap_lowerFactorMap_le (n : ℕ) :
 theorem measurable_lowerFactorMap' (n : ℕ) : Measurable (B.lowerFactorMap n) :=
   (B.measurable_lowerFactorMap n).mono (RelStructure.lowerRankAlgebra_le n) le_rfl
 
+/-! ### Rank nesting -/
+
+/-- The index embedding for `n ≤ m`: a smaller rank bound admits fewer coordinates. -/
+def lowerIndexEmbedding {n m : ℕ} (h : n ≤ m) : B.LowerIndex n → B.LowerIndex m :=
+  fun i => ⟨i.1, lt_of_lt_of_le i.2 h⟩
+
+/-- The factor projection for `n ≤ m`: ordinary coordinate restriction. -/
+def lowerFactorProjection {n m : ℕ} (h : n ≤ m) :
+    B.LowerFactorSpace m → B.LowerFactorSpace n :=
+  fun f => f ∘ B.lowerIndexEmbedding h
+
+theorem measurable_lowerFactorProjection {n m : ℕ} (h : n ≤ m) :
+    Measurable (B.lowerFactorProjection h) :=
+  measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+open scoped Classical in
+/-- **The projection is compatible with the factor maps** — definitional, since both sides read
+the same coordinates. -/
+theorem lowerFactorProjection_lowerFactorMap {n m : ℕ} (h : n ≤ m) :
+    B.lowerFactorProjection h ∘ B.lowerFactorMap m = B.lowerFactorMap n := rfl
+
+/-- **The projection cocycle**, likewise definitional. -/
+theorem lowerFactorProjection_comp {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) :
+    B.lowerFactorProjection hnm ∘ B.lowerFactorProjection hmk =
+      B.lowerFactorProjection (hnm.trans hmk) := rfl
+
+/-! ### Restriction to a single support -/
+
+/-- Every coordinate anchored inside `A` has rank below `n`, when `A` itself does. -/
+def basisIndexToLowerIndex {A : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ}
+    (hA : A.card < n) : B.BasisIndex A → B.LowerIndex n :=
+  fun i => ⟨i.1, lt_of_le_of_lt (Finset.card_le_card i.2) hA⟩
+
+/-- **The finite-factor projection**: restrict the lower-rank factor to the coordinates of a
+single support of rank `< n`. This is the device that lets the generation argument work support
+by support, rather than trying to assemble representatives through the `iSup`. -/
+def lowerToFactorProjection {A : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ}
+    (hA : A.card < n) : B.LowerFactorSpace n → B.FactorSpace A :=
+  fun f => f ∘ B.basisIndexToLowerIndex hA
+
+theorem measurable_lowerToFactorProjection {A : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ}
+    (hA : A.card < n) : Measurable (B.lowerToFactorProjection hA) :=
+  measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+open scoped Classical in
+/-- **Compatibility with the single-support factor map**, definitional: reading the `A`-anchored
+coordinates of the lower-rank factor *is* the factor map at `A`. -/
+theorem lowerToFactorProjection_lowerFactorMap {A : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ}
+    (hA : A.card < n) :
+    B.lowerToFactorProjection hA ∘ B.lowerFactorMap n = B.factorMap A := rfl
+
 end CoherentBasis
 
 end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index 6fbb9d6..fd840b7 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -216,3 +216,8 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.CoherentBasis.measurable_lowerFactorMap
 #print axioms RelSignature.CoherentBasis.comap_lowerFactorMap_le
 #print axioms RelSignature.CoherentBasis.measurable_lowerFactorMap'
+#print axioms RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorMap
+#print axioms RelSignature.CoherentBasis.lowerFactorProjection_comp
+#print axioms RelSignature.CoherentBasis.lowerToFactorProjection_lowerFactorMap
+#print axioms RelSignature.CoherentBasis.measurable_lowerFactorProjection
+#print axioms RelSignature.CoherentBasis.measurable_lowerToFactorProjection
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 79b60e8..02ba50b 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -199,6 +199,11 @@
     "RelSignature.CoherentBasis.measurable_lowerFactorMap",
     "RelSignature.CoherentBasis.comap_lowerFactorMap_le",
     "RelSignature.CoherentBasis.measurable_lowerFactorMap'",
+    "RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorMap",
+    "RelSignature.CoherentBasis.lowerFactorProjection_comp",
+    "RelSignature.CoherentBasis.lowerToFactorProjection_lowerFactorMap",
+    "RelSignature.CoherentBasis.measurable_lowerFactorProjection",
+    "RelSignature.CoherentBasis.measurable_lowerToFactorProjection",
     "RelSignature.condExp_ae_eq_condExp_of_comap_eq",
     "RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel",
     "RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra",

From 67863d9356e1aeda9f803428ef305dfb7aa6d570 Mon Sep 17 00:00:00 2001
From: Cameron Freer <freer@mit.edu>
Date: Fri, 31 Jul 2026 01:57:49 +0000
Subject: [PATCH 3/4] feat: cond-indep layer 3, lower-factor generation +
 equivariance (#107)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Completes the structural lower-rank factor.

* `comap_factorMap_le_comap_lowerFactorMap`: for `A.card < n` the single-support
  pullback sits inside the lower-rank pullback, via `lowerToFactorProjection`.
* `exists_comap_lowerFactorMap_ae_eq`: every `lowerRankAlgebra n` event has an
  a.e. representative read off the lower-rank factor. Proved support by support
  and joined inside `eventuallyMeasurableSpace`, so the completion does the
  closing — no simultaneous choice of a.e. witnesses through the `iSup`.
  Stated eventwise; the two σ-algebras are not equal, and 'equal modulo null
  sets' would commit to a trim/completion identification that is unavailable.
* `lowerIndexEquiv` + `comap_relabel_comap_lowerFactorMap`: FinSuppPerm
  equivariance, the factor-level counterpart of comap_relabel_lowerRankAlgebra.
* `comap_lowerFactorMap_zero`: rank zero is `⊥` on the nose, not modulo the law.
* `exists_comap_lowerFactorMap_one_ae_eq`: the rank-one base, on the original
  law — no augmented space, no coupling.

Audit 218 -> 224.
---
 Graphon/RelLowerFactor.lean        | 174 +++++++++++++++++++++++++++++
 scripts/axiom_audit.lean           |   6 +
 scripts/check_census_and_axioms.py |   6 +
 3 files changed, 186 insertions(+)

diff --git a/Graphon/RelLowerFactor.lean b/Graphon/RelLowerFactor.lean
index c88796c..95e2f96 100644
--- a/Graphon/RelLowerFactor.lean
+++ b/Graphon/RelLowerFactor.lean
@@ -34,6 +34,25 @@ same discipline as everywhere else in this layer, and for the same reason.
 `LowerIndex n` is not closed under the Boolean operations: two small anchors can combine to a
 large one. That is not a defect and no closure should be engineered — the product σ-algebra on
 `LowerFactorSpace n` still contains Boolean combinations of the coordinates.
+
+## How generation is proved
+
+Support by support, never through the `iSup`. The finite-factor projection
+`lowerToFactorProjection` exhibits `factorMap A` as a coordinate restriction of
+`lowerFactorMap n` whenever `A.card < n`, so `exists_comap_factorMap_ae_eq` already gives a
+representative measurable for the lower-rank factor. The containments are then joined inside
+`eventuallyMeasurableSpace`, which is a σ-algebra: the completion is the closure device, and no
+family of a.e. witnesses is ever chosen simultaneously.
+
+## Contents
+
+* `LowerIndex` / `LowerFactorSpace` / `lowerFactorMap`, with `comap_lowerFactorMap_le`;
+* `lowerFactorProjection` and `lowerToFactorProjection` — rank nesting and single-support
+  restriction, whose compatibilities with the factor maps are definitional;
+* `exists_comap_lowerFactorMap_ae_eq` — the eventwise converse to `comap_lowerFactorMap_le`;
+* `lowerIndexEquiv` / `comap_relabel_comap_lowerFactorMap` — `FinSuppPerm` equivariance;
+* `comap_lowerFactorMap_zero` (raw, `⊥`) and `exists_comap_lowerFactorMap_one_ae_eq` (the
+  rank-one base, on the original law).
 -/
 
 open MeasureTheory MeasurableSpace
@@ -150,6 +169,161 @@ theorem lowerToFactorProjection_lowerFactorMap {A : Finset (Σ s : S.Srt, Vinfin
     (hA : A.card < n) :
     B.lowerToFactorProjection hA ∘ B.lowerFactorMap n = B.factorMap A := rfl
 
+/-! ### Generation -/
+
+open scoped Classical in
+/-- Coordinates anchored in a support of rank `< n` are read by the lower-rank factor: the
+single-support pullback sits inside the lower-rank pullback. -/
+theorem comap_factorMap_le_comap_lowerFactorMap
+    {A : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ} (hA : A.card < n) :
+    MeasurableSpace.comap (B.factorMap A) inferInstance ≤
+      MeasurableSpace.comap (B.lowerFactorMap n) inferInstance := by
+  rw [← B.lowerToFactorProjection_lowerFactorMap hA, ← MeasurableSpace.comap_comp]
+  exact MeasurableSpace.comap_mono (B.measurable_lowerToFactorProjection hA).comap_le
+
+open scoped Classical in
+/-- Every event of a low-rank fixing algebra has a representative measurable for the lower-rank
+factor. This is proved support by support, through `lowerToFactorProjection`; assembling
+representatives directly through the `iSup` would require simultaneous a.e. choices and is not
+what happens here. -/
+theorem fixingAlgebra_le_eventually_comap_lowerFactorMap
+    {A : Finset (Σ s : S.Srt, Vinfinite S s)} {n : ℕ} (hA : A.card < n) :
+    RelStructure.fixingAlgebra A ≤
+      eventuallyMeasurableSpace (MeasurableSpace.comap (B.lowerFactorMap n) inferInstance)
+        (ae (M.law : Measure (RelStructure S (Vinfinite S)))) := by
+  intro E hE
+  obtain ⟨E', hE'meas, hE'ae⟩ := B.exists_comap_factorMap_ae_eq A hE
+  exact ⟨E', B.comap_factorMap_le_comap_lowerFactorMap hA _ hE'meas, hE'ae.symm⟩
+
+open scoped Classical in
+/-- **The lower-rank conditioning algebra is contained in the completed lower-rank factor.**
+Taking the `iSup` is legitimate here precisely because the containment is into a σ-algebra —
+the completion is the closure device, so no a.e. witnesses are ever joined. -/
+theorem lowerRankAlgebra_le_eventually_comap_lowerFactorMap (n : ℕ) :
+    RelStructure.lowerRankAlgebra (S := S) n ≤
+      eventuallyMeasurableSpace (MeasurableSpace.comap (B.lowerFactorMap n) inferInstance)
+        (ae (M.law : Measure (RelStructure S (Vinfinite S)))) :=
+  iSup₂_le fun _ hA => B.fixingAlgebra_le_eventually_comap_lowerFactorMap hA
+
+open scoped Classical in
+/-- **The eventwise converse to `comap_lowerFactorMap_le`**: every event of the lower-rank
+conditioning algebra agrees, up to a null set, with an event read off the lower-rank factor.
+
+Stated eventwise on purpose. The two σ-algebras are *not* equal — `lowerRankAlgebra` is
+law-free while the factor is only determined modulo `M.law` — and phrasing the converse as an
+equality "modulo null sets" would commit to a `trim`/`completion` identification that is not
+available. -/
+theorem exists_comap_lowerFactorMap_ae_eq (n : ℕ)
+    {E : Set (RelStructure S (Vinfinite S))}
+    (hE : MeasurableSet[RelStructure.lowerRankAlgebra (S := S) n] E) :
+    ∃ E', MeasurableSet[MeasurableSpace.comap (B.lowerFactorMap n) inferInstance] E' ∧
+      E' =ᵐ[(M.law : Measure (RelStructure S (Vinfinite S)))] E := by
+  obtain ⟨E', hE'meas, hE'ae⟩ := B.lowerRankAlgebra_le_eventually_comap_lowerFactorMap n E hE
+  exact ⟨E', hE'meas, hE'ae.symm⟩
+
+/-! ### Equivariance -/
+
+private theorem sigmaMap_inj (σ : FinSuppPerm S) :
+    Function.Injective (Sigma.map id fun s => ⇑(σ.1 s) :
+      (Σ s : S.Srt, Vinfinite S s) → Σ s : S.Srt, Vinfinite S s) := by
+  have hinv : Function.LeftInverse
+      (Sigma.map id fun s => ⇑((σ⁻¹ : FinSuppPerm S).1 s) :
+        (Σ s : S.Srt, Vinfinite S s) → Σ s : S.Srt, Vinfinite S s)
+      (Sigma.map id fun s => ⇑(σ.1 s)) := by
+    rintro ⟨s, x⟩
+    show (⟨s, (σ⁻¹ : FinSuppPerm S).1 s (σ.1 s x)⟩ : Σ s : S.Srt, Vinfinite S s) = ⟨s, x⟩
+    rw [show (σ⁻¹ : FinSuppPerm S).1 s (σ.1 s x) = x from (σ.1 s).symm_apply_apply x]
+  exact hinv.injective
+
+open scoped Classical in
+/-- **A relabeling as an equivalence of the lower-rank index.** Unlike `basisIndexEquiv`, this
+is an equivalence of a *single* type: a relabeling transports anchors by an injective image map,
+so it preserves cardinality and hence rank. -/
+noncomputable def lowerIndexEquiv (σ : FinSuppPerm S) (n : ℕ) :
+    B.LowerIndex n ≃ B.LowerIndex n where
+  toFun i := ⟨B.act σ i.1, by
+    rw [B.anchor_act, Finset.card_image_of_injective _ (sigmaMap_inj σ)]; exact i.2⟩
+  invFun j := ⟨B.act σ⁻¹ j.1, by
+    rw [B.anchor_act, Finset.card_image_of_injective _ (sigmaMap_inj σ⁻¹)]; exact j.2⟩
+  left_inv i := Subtype.ext (by
+    show B.act σ⁻¹ (B.act σ i.1) = i.1
+    rw [← B.act_mul, inv_mul_cancel, B.act_one])
+  right_inv j := Subtype.ext (by
+    show B.act σ (B.act σ⁻¹ j.1) = j.1
+    rw [← B.act_mul, mul_inv_cancel, B.act_one])
+
+open scoped Classical in
+/-- **Naturality of the lower-rank factor map**, with the orientation forced, as for
+`factorMap_basisIndexEquiv`, by `event_act` being a preimage equality. -/
+theorem lowerFactorMap_lowerIndexEquiv (σ : FinSuppPerm S) (n : ℕ)
+    (X : RelStructure S (Vinfinite S)) (i : B.LowerIndex n) :
+    B.lowerFactorMap n X (B.lowerIndexEquiv σ n i) =
+      B.lowerFactorMap n (RelStructure.relabel σ.1 X) i := by
+  show decide (X ∈ B.event (B.act σ i.1)) = decide (RelStructure.relabel σ.1 X ∈ B.event i.1)
+  rw [B.event_act]
+  rfl
+
+open scoped Classical in
+/-- **A relabeling as a measurable automorphism of the lower-rank factor space**, namely
+coordinate reindexing along `lowerIndexEquiv`. -/
+noncomputable def lowerFactorSpaceEquiv (σ : FinSuppPerm S) (n : ℕ) :
+    B.LowerFactorSpace n ≃ᵐ B.LowerFactorSpace n where
+  toEquiv := Equiv.arrowCongr (B.lowerIndexEquiv σ n).symm (Equiv.refl Bool)
+  measurable_toFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+  measurable_invFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
+
+open scoped Classical in
+/-- The relabeling of a structure is read by the factor through that automorphism. -/
+theorem lowerFactorSpaceEquiv_comp_lowerFactorMap (σ : FinSuppPerm S) (n : ℕ) :
+    B.lowerFactorSpaceEquiv σ n ∘ B.lowerFactorMap n =
+      B.lowerFactorMap n ∘ RelStructure.relabel σ.1 :=
+  funext fun X => funext fun i => B.lowerFactorMap_lowerIndexEquiv σ n X i
+
+open scoped Classical in
+/-- **The lower-rank factor pullback is relabeling invariant** under the finitely supported
+relabelings — the factor-level counterpart of
+`RelStructure.comap_relabel_lowerRankAlgebra`, which is what makes the pullback a legitimate
+conditioning factor for an exchangeable law. -/
+theorem comap_relabel_comap_lowerFactorMap (σ : FinSuppPerm S) (n : ℕ) :
+    MeasurableSpace.comap (RelStructure.relabel σ.1)
+        (MeasurableSpace.comap (B.lowerFactorMap n) inferInstance) =
+      MeasurableSpace.comap (B.lowerFactorMap n) inferInstance := by
+  have hcomap : MeasurableSpace.comap (⇑(B.lowerFactorSpaceEquiv σ n))
+      (inferInstance : MeasurableSpace (B.LowerFactorSpace n)) =
+        (inferInstance : MeasurableSpace (B.LowerFactorSpace n)) := by
+    refine le_antisymm (B.lowerFactorSpaceEquiv σ n).measurable.comap_le fun s hs => ?_
+    refine ⟨(B.lowerFactorSpaceEquiv σ n).symm ⁻¹' s,
+      (B.lowerFactorSpaceEquiv σ n).symm.measurable hs, ?_⟩
+    ext x
+    simp
+  rw [MeasurableSpace.comap_comp, ← B.lowerFactorSpaceEquiv_comp_lowerFactorMap,
+    ← MeasurableSpace.comap_comp, hcomap]
+
+/-! ### The degenerate ranks -/
+
+open scoped Classical in
+/-- **Rank zero is trivial on the nose** — not merely modulo the law. There are no coordinates
+of rank below `0`, so the factor space is a point and its pullback is `⊥`. -/
+theorem comap_lowerFactorMap_zero :
+    MeasurableSpace.comap (B.lowerFactorMap 0) inferInstance = ⊥ := by
+  refine le_antisymm (fun E hE => ?_) bot_le
+  obtain ⟨t, -, rfl⟩ := hE
+  rcases Set.eq_empty_or_nonempty t with rfl | ⟨y, hy⟩
+  · simp
+  · rw [show t = Set.univ from Set.eq_univ_of_forall fun z => Subsingleton.elim z y ▸ hy]
+    simp
+
+open scoped Classical in
+/-- **Rank one**: every invariant event agrees with an event of the rank-one factor, up to a
+null set. This is the base of the rank recursion, stated on the original law — no augmented
+space and no coupling. -/
+theorem exists_comap_lowerFactorMap_one_ae_eq
+    {E : Set (RelStructure S (Vinfinite S))}
+    (hE : MeasurableSet[RelStructure.invariantAlgebra (S := S)] E) :
+    ∃ E', MeasurableSet[MeasurableSpace.comap (B.lowerFactorMap 1) inferInstance] E' ∧
+      E' =ᵐ[(M.law : Measure (RelStructure S (Vinfinite S)))] E :=
+  B.exists_comap_lowerFactorMap_ae_eq 1 (by rwa [RelStructure.lowerRankAlgebra_one])
+
 end CoherentBasis
 
 end RelSignature
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index fd840b7..f1be70e 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -221,3 +221,9 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.CoherentBasis.lowerToFactorProjection_lowerFactorMap
 #print axioms RelSignature.CoherentBasis.measurable_lowerFactorProjection
 #print axioms RelSignature.CoherentBasis.measurable_lowerToFactorProjection
+#print axioms RelSignature.CoherentBasis.comap_factorMap_le_comap_lowerFactorMap
+#print axioms RelSignature.CoherentBasis.exists_comap_lowerFactorMap_ae_eq
+#print axioms RelSignature.CoherentBasis.lowerFactorMap_lowerIndexEquiv
+#print axioms RelSignature.CoherentBasis.comap_relabel_comap_lowerFactorMap
+#print axioms RelSignature.CoherentBasis.comap_lowerFactorMap_zero
+#print axioms RelSignature.CoherentBasis.exists_comap_lowerFactorMap_one_ae_eq
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 02ba50b..216b6e2 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -204,6 +204,12 @@
     "RelSignature.CoherentBasis.lowerToFactorProjection_lowerFactorMap",
     "RelSignature.CoherentBasis.measurable_lowerFactorProjection",
     "RelSignature.CoherentBasis.measurable_lowerToFactorProjection",
+    "RelSignature.CoherentBasis.comap_factorMap_le_comap_lowerFactorMap",
+    "RelSignature.CoherentBasis.exists_comap_lowerFactorMap_ae_eq",
+    "RelSignature.CoherentBasis.lowerFactorMap_lowerIndexEquiv",
+    "RelSignature.CoherentBasis.comap_relabel_comap_lowerFactorMap",
+    "RelSignature.CoherentBasis.comap_lowerFactorMap_zero",
+    "RelSignature.CoherentBasis.exists_comap_lowerFactorMap_one_ae_eq",
     "RelSignature.condExp_ae_eq_condExp_of_comap_eq",
     "RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel",
     "RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra",

From 715eced9148cf6779a765c83866994f77713bbfa Mon Sep 17 00:00:00 2001
From: Cameron Freer <freer@mit.edu>
Date: Fri, 31 Jul 2026 02:27:29 +0000
Subject: [PATCH 4/4] docs+feat: reviewer follow-ups on the lower-rank factor
 (#107)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* `Graphon.lean`: add the missing `Graphon.RelLowerFactor` inventory entry.
* Soften the raw-equality wording in the module and theorem docstrings: no raw
  equality is asserted or supplied by this construction, and the available
  converse is eventwise modulo `M.law`. Nothing here shows the two σ-algebras
  are unequal, and the docstrings no longer suggest otherwise.
* Add the nesting/equivariance square
  `lowerFactorProjection h ∘ lowerFactorSpaceEquiv σ m =
     lowerFactorSpaceEquiv σ n ∘ lowerFactorProjection h`,
  definitional up to proof irrelevance in the rank bound. Without it the
  relabeling action would not descend along the nesting maps.
* Add identity and multiplication laws for `lowerIndexEquiv` and
  `lowerFactorSpaceEquiv`. These are automorphisms of one fixed type, unlike
  `basisIndexEquiv`, so they are honest equalities of equivalences rather than
  underlying-index laws; reindexing is contravariant, so the factor-space
  composition law reverses the order.

Audit 224 -> 227.
---
 Graphon.lean                       |  1 +
 Graphon/RelLowerFactor.lean        | 68 +++++++++++++++++++++++++++---
 scripts/axiom_audit.lean           |  3 ++
 scripts/check_census_and_axioms.py |  3 ++
 4 files changed, 69 insertions(+), 6 deletions(-)

diff --git a/Graphon.lean b/Graphon.lean
index 5a41d02..5c11bb6 100644
--- a/Graphon.lean
+++ b/Graphon.lean
@@ -208,6 +208,7 @@ in Lean 4 using Mathlib.
 * `Graphon.RelFactorLaws` — R4 converse piece 3 (#107): the boundary/exact splitting of the coherent factors and their laws. `BoundaryIndex A` collects indices anchored *properly* inside `A` and `ExactIndex A` the exact-anchor layer, giving the measurable equivalence `FactorSpace A ≃ᵐ BoundarySpace A × ExactSpace A`. This partitions *coordinates by anchor*, not information: anchors are not minimal, so an expression anchored at `A` may still name an event measurable over a proper subset. This is the shape the AHK recursion needs — one kernel per finite `A`, conditioned on the whole proper-subset boundary and recursing by `|A|`: kernels for every pair `C ⊆ A` would be redundant and force compatibility between different a.e. versions of conditional distributions, while a linear chain would impose an arbitrary ordering and let the value at `A` depend on sets incomparable to it, breaking subset-locality. `factorLaw` / `boundaryLaw` / `exactLaw` are the pushforwards, with projection consistency along the sub-index inclusions and relabeling invariance from exchangeability — the first place in this layer where the law is used
 * `Graphon.RelStepKernel` — R4 converse piece 3 (#107): **one kernel per finite `A`**, `stepKernel A : Kernel (BoundarySpace A) (ExactSpace A)`, the conditional distribution of the exact-anchor layer given the whole proper-subset boundary — not one kernel per pair `C ⊆ A`, and not a chain. Built as `condDistrib`, whose standard-Borel hypothesis is exactly what the factor-space packaging supplies. Central identities: the disintegration `boundaryLaw A ⊗ₘ stepKernel A = M.law.map (boundaryMap A, exactMap A)`, marginal recovery `stepKernel A ∘ₘ boundaryLaw A = exactLaw A`, and the same read through `factorSpaceProdEquiv`. Valid for an arbitrary exchangeable law; the `A = ∅` base case is deliberately absent, since its determinism uses dissociation and belongs to the later realization layer
 * `Graphon.RelRankAlgebra` — R4 converse piece 3 (#107): the **lower-rank conditioning algebra** `lowerRankAlgebra n = ⨆ A, ⨆ (_ : A.card < n), fixingAlgebra A` and its order theory — monotone in the rank bound, below the ambient algebra, containing each low-rank fixing algebra, `⊥` at rank `0`, and `invariantAlgebra` at rank `1` (the recursion's base, and the reason no `NoNullary` hypothesis is needed). Plus `comap_relabel_lowerRankAlgebra`, invariance under an **arbitrary** sortwise permutation family — relabelings displacing infinitely many vertices arise naturally downstream, so the finite-support hypothesis would be too weak — and `card_inter_lt_of_ne`, that distinct supports of equal rank meet in strictly lower rank. Law-free throughout
+* `Graphon.RelLowerFactor` — R4 converse piece 3 (#107): the **structural lower-rank factor**, the object the rank recursion conditions on. `lowerFactorMap n` reads the coherent-basis coordinates whose anchor has cardinality `< n` into the standard Borel `LowerFactorSpace n`. It is stated about the *factor*, never about latents: a latent normally carries randomness beyond the factor it represents — already `1_{U < p}` generates strictly less than `U` — so a σ-algebra generated by latents is typically strictly larger. Generation is `comap (lowerFactorMap n) inferInstance ≤ lowerRankAlgebra n` together with an **eventwise** converse; no raw equality is asserted or supplied, the available converse being modulo `M.law`. The converse is proved support by support through `lowerToFactorProjection`, which exhibits `factorMap A` as a coordinate restriction whenever `A.card < n`, and the containments are joined inside `eventuallyMeasurableSpace` — already a σ-algebra, so the completion does the closing and no family of a.e. witnesses is ever chosen simultaneously through the `iSup`. `lowerIndexEquiv` gives `FinSuppPerm` equivariance as automorphisms of one fixed type (rank is preserved because anchors transport by an injective image map), so the action laws are honest equalities of equivalences with no dependent transport, and they commute with rank nesting definitionally. Rank `0` is `⊥` on the nose; rank `1` is the recursion's base, on the original law, with no augmented space and no coupling
 * `Graphon.DigraphMaps` — the minimal `Digraph.comap` pullback API for Mathlib's `Digraph` (mirroring `SimpleGraph.comap`; a Mathlib-upstream candidate tracked on #24), used by the D2 directed-law bridge
 * `Graphon.InfiniteDigraphLaw` — Directed umbrella (#84) D2 (#86): the `PMF`-based finite directed law `ExchangeableDigraphLaw` (consistent under `Digraph.comap`), the finite bridge `digraphLawEquiv : ExchangeableDigraphLaw ≃ RelExchangeableLaw digraphSig` (via `finiteDigraphEquiv` + `PMF.toMeasure`/`Measure.toPMF`), and the headline `exchangeableDigraphLawEquiv : ExchangeableDigraphLaw ≃ InfiniteExchangeableDigraphLaw` composing with R2c — measurable structure stays on the relational carrier
 * `Graphon.ExchangeableLawBlueprint` — annotation-only blueprint wrappers for the R2c relational (`relExchangeableLawEquiv`) and D2 directed (`exchangeableDigraphLawEquiv`) equivalences, keeping `Architect` out of the reusable foundational modules
diff --git a/Graphon/RelLowerFactor.lean b/Graphon/RelLowerFactor.lean
index 95e2f96..b392e5f 100644
--- a/Graphon/RelLowerFactor.lean
+++ b/Graphon/RelLowerFactor.lean
@@ -28,8 +28,9 @@ Only
 
 `comap (lowerFactorMap n) inferInstance ≤ lowerRankAlgebra n`
 
-together with an eventwise mod-null converse. **No raw equality of measurable spaces** — the
-same discipline as everywhere else in this layer, and for the same reason.
+together with an eventwise mod-null converse. No raw equality is asserted or supplied by this
+construction; the available converse is eventwise modulo `M.law`. That is the same discipline as
+everywhere else in this layer, and for the same reason.
 
 `LowerIndex n` is not closed under the Boolean operations: two small anchors can combine to a
 large one. That is not a defect and no closure should be engineered — the product σ-algebra on
@@ -50,7 +51,9 @@ family of a.e. witnesses is ever chosen simultaneously.
 * `lowerFactorProjection` and `lowerToFactorProjection` — rank nesting and single-support
   restriction, whose compatibilities with the factor maps are definitional;
 * `exists_comap_lowerFactorMap_ae_eq` — the eventwise converse to `comap_lowerFactorMap_le`;
-* `lowerIndexEquiv` / `comap_relabel_comap_lowerFactorMap` — `FinSuppPerm` equivariance;
+* `lowerIndexEquiv` / `comap_relabel_comap_lowerFactorMap` — `FinSuppPerm` equivariance, with
+  the action laws as honest equalities of equivalences and the nesting square
+  `lowerFactorProjection_lowerFactorSpaceEquiv`;
 * `comap_lowerFactorMap_zero` (raw, `⊥`) and `exists_comap_lowerFactorMap_one_ae_eq` (the
   rank-one base, on the original law).
 -/
@@ -209,9 +212,10 @@ open scoped Classical in
 /-- **The eventwise converse to `comap_lowerFactorMap_le`**: every event of the lower-rank
 conditioning algebra agrees, up to a null set, with an event read off the lower-rank factor.
 
-Stated eventwise on purpose. The two σ-algebras are *not* equal — `lowerRankAlgebra` is
-law-free while the factor is only determined modulo `M.law` — and phrasing the converse as an
-equality "modulo null sets" would commit to a `trim`/`completion` identification that is not
+Stated eventwise on purpose. No raw equality is asserted or supplied by this construction; the
+available converse is eventwise modulo `M.law`. Nothing here rules out an equality of the two
+σ-algebras — the point is that this argument does not produce one, and phrasing the converse as
+an equality "modulo null sets" would commit to a `trim`/`completion` identification that is not
 available. -/
 theorem exists_comap_lowerFactorMap_ae_eq (n : ℕ)
     {E : Set (RelStructure S (Vinfinite S))}
@@ -252,6 +256,28 @@ noncomputable def lowerIndexEquiv (σ : FinSuppPerm S) (n : ℕ) :
     show B.act σ (B.act σ⁻¹ j.1) = j.1
     rw [← B.act_mul, mul_inv_cancel, B.act_one])
 
+open scoped Classical in
+@[simp] theorem lowerIndexEquiv_apply_coe (σ : FinSuppPerm S) (n : ℕ) (i : B.LowerIndex n) :
+    (B.lowerIndexEquiv σ n i).1 = B.act σ i.1 := rfl
+
+open scoped Classical in
+@[simp] theorem lowerIndexEquiv_symm_apply_coe (σ : FinSuppPerm S) (n : ℕ) (j : B.LowerIndex n) :
+    ((B.lowerIndexEquiv σ n).symm j).1 = B.act σ⁻¹ j.1 := rfl
+
+open scoped Classical in
+/-- **Identity**, as an honest equality of equivalences. Unlike `basisIndexEquiv`, whose codomain
+`BasisIndex (A.image σ)` varies with `σ`, these are automorphisms of one fixed type, so the
+action laws need no dependent transport. -/
+@[simp] theorem lowerIndexEquiv_one (n : ℕ) :
+    B.lowerIndexEquiv (1 : FinSuppPerm S) n = Equiv.refl _ :=
+  Equiv.ext fun i => Subtype.ext (B.act_one i.1)
+
+open scoped Classical in
+/-- **Composition**, likewise an honest equality of equivalences. -/
+@[simp] theorem lowerIndexEquiv_mul (σ τ : FinSuppPerm S) (n : ℕ) :
+    B.lowerIndexEquiv (σ * τ) n = (B.lowerIndexEquiv τ n).trans (B.lowerIndexEquiv σ n) :=
+  Equiv.ext fun i => Subtype.ext (B.act_mul σ τ i.1)
+
 open scoped Classical in
 /-- **Naturality of the lower-rank factor map**, with the orientation forced, as for
 `factorMap_basisIndexEquiv`, by `event_act` being a preimage equality. -/
@@ -272,6 +298,36 @@ noncomputable def lowerFactorSpaceEquiv (σ : FinSuppPerm S) (n : ℕ) :
   measurable_toFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
   measurable_invFun := measurable_pi_lambda _ fun _ => measurable_pi_apply _
 
+open scoped Classical in
+@[simp] theorem lowerFactorSpaceEquiv_apply (σ : FinSuppPerm S) (n : ℕ)
+    (g : B.LowerFactorSpace n) (i : B.LowerIndex n) :
+    B.lowerFactorSpaceEquiv σ n g i = g (B.lowerIndexEquiv σ n i) := rfl
+
+open scoped Classical in
+/-- The identity acts trivially. Reindexing is contravariant, so the composition law below
+reverses the order. -/
+@[simp] theorem lowerFactorSpaceEquiv_one (n : ℕ) :
+    B.lowerFactorSpaceEquiv (1 : FinSuppPerm S) n = MeasurableEquiv.refl _ :=
+  MeasurableEquiv.ext <| funext fun g => funext fun i => by simp
+
+open scoped Classical in
+@[simp] theorem lowerFactorSpaceEquiv_mul (σ τ : FinSuppPerm S) (n : ℕ) :
+    B.lowerFactorSpaceEquiv (σ * τ) n =
+      (B.lowerFactorSpaceEquiv σ n).trans (B.lowerFactorSpaceEquiv τ n) :=
+  MeasurableEquiv.ext <| funext fun g => funext fun i => by simp
+
+open scoped Classical in
+/-- **The nesting/equivariance square**: restricting the rank commutes with relabeling. Both
+sides read the coordinate `act σ i` of the same argument, so the identity is definitional up to
+proof irrelevance in the rank bound.
+
+This is the structural coherence the rank recursion needs: without it, the relabeling action on
+the lower-rank factors would not descend along the nesting maps, and the actions at different
+ranks would be unrelated. -/
+theorem lowerFactorProjection_lowerFactorSpaceEquiv (σ : FinSuppPerm S) {n m : ℕ} (h : n ≤ m) :
+    B.lowerFactorProjection h ∘ B.lowerFactorSpaceEquiv σ m =
+      B.lowerFactorSpaceEquiv σ n ∘ B.lowerFactorProjection h := rfl
+
 open scoped Classical in
 /-- The relabeling of a structure is read by the factor through that automorphism. -/
 theorem lowerFactorSpaceEquiv_comp_lowerFactorMap (σ : FinSuppPerm S) (n : ℕ) :
diff --git a/scripts/axiom_audit.lean b/scripts/axiom_audit.lean
index f1be70e..fae6690 100644
--- a/scripts/axiom_audit.lean
+++ b/scripts/axiom_audit.lean
@@ -227,3 +227,6 @@ custom axioms. Target list and policy: `scripts/check_census_and_axioms.py`
 #print axioms RelSignature.CoherentBasis.comap_relabel_comap_lowerFactorMap
 #print axioms RelSignature.CoherentBasis.comap_lowerFactorMap_zero
 #print axioms RelSignature.CoherentBasis.exists_comap_lowerFactorMap_one_ae_eq
+#print axioms RelSignature.CoherentBasis.lowerIndexEquiv_mul
+#print axioms RelSignature.CoherentBasis.lowerFactorSpaceEquiv_mul
+#print axioms RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorSpaceEquiv
diff --git a/scripts/check_census_and_axioms.py b/scripts/check_census_and_axioms.py
index 216b6e2..a8b2c95 100644
--- a/scripts/check_census_and_axioms.py
+++ b/scripts/check_census_and_axioms.py
@@ -210,6 +210,9 @@
     "RelSignature.CoherentBasis.comap_relabel_comap_lowerFactorMap",
     "RelSignature.CoherentBasis.comap_lowerFactorMap_zero",
     "RelSignature.CoherentBasis.exists_comap_lowerFactorMap_one_ae_eq",
+    "RelSignature.CoherentBasis.lowerIndexEquiv_mul",
+    "RelSignature.CoherentBasis.lowerFactorSpaceEquiv_mul",
+    "RelSignature.CoherentBasis.lowerFactorProjection_lowerFactorSpaceEquiv",
     "RelSignature.condExp_ae_eq_condExp_of_comap_eq",
     "RelSignature.InfiniteRelExchangeableLaw.measurePreserving_relabel",
     "RelSignature.InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra",