diff --git a/Graphon.lean b/Graphon.lean index 86e297b..5c11bb6 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 @@ -207,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 new file mode 100644 index 0000000..b392e5f --- /dev/null +++ b/Graphon/RelLowerFactor.lean @@ -0,0 +1,385 @@ +/- +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 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 +`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, 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). +-/ + +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 + +/-! ### 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 + +/-! ### 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. 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))} + (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 +@[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. -/ +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 +@[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 : ℕ) : + 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 72d0f25..fae6690 100644 --- a/scripts/axiom_audit.lean +++ b/scripts/axiom_audit.lean @@ -213,3 +213,20 @@ 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' +#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 +#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 +#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 9117982..a8b2c95 100644 --- a/scripts/check_census_and_axioms.py +++ b/scripts/check_census_and_axioms.py @@ -196,6 +196,23 @@ "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.CoherentBasis.lowerFactorProjection_lowerFactorMap", + "RelSignature.CoherentBasis.lowerFactorProjection_comp", + "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.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",