feat: the structural lower-rank factor (#107 converse piece 3) - #157
Merged
Conversation
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.
…tion (#107) 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.
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.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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The structural lower-rank factor for the rank induction. No coupling construction, no augmented probability space, no
ξ_∅— those belong to the next layer, which should consume a settled factor API rather than be mixed with it.Graphon/RelLowerFactor.lean, built on the coherent basis:LowerIndex n/LowerFactorSpace n/lowerFactorMap n— the basis coordinates whose anchor has cardinality< n, as a standard Borel factor. Everything is stated about the factor, not about latents: a latent normally carries randomness beyond the factor it represents (already1_{U < p}generates strictly less thanU), soσ(latents)is typically strictly larger.comap_lowerFactorMap_le— the pullback sits insidelowerRankAlgebra n.lowerFactorProjection(rank nesting) andlowerToFactorProjection(single-support restriction), with the compatibilities againstlowerFactorMap/factorMapand the cocycle law all definitional.exists_comap_lowerFactorMap_ae_eq— the eventwise converse. Proved support by support throughlowerToFactorProjectionandexists_comap_factorMap_ae_eq, with the containments joined insideeventuallyMeasurableSpace. The completion is the closure device, so no family of a.e. witnesses is ever chosen simultaneously through theiSup.lowerIndexEquiv,comap_relabel_comap_lowerFactorMap—FinSuppPermequivariance, the factor-level counterpart ofRelStructure.comap_relabel_lowerRankAlgebra.lowerFactorProjection_lowerFactorSpaceEquiv— the nesting/equivariance square, definitional up to proof irrelevance in the rank bound: without it the relabeling action would not descend along the nesting maps. Identity and multiplication laws forlowerIndexEquiv/lowerFactorSpaceEquivcome as honest equalities of equivalences, since these are automorphisms of one fixed type unlikebasisIndexEquiv.comap_lowerFactorMap_zero— rank zero is⊥on the nose, not modulo the law.exists_comap_lowerFactorMap_one_ae_eq— the rank-one base, rewritten throughlowerRankAlgebra_one, on the original law.On raw equality
The generation API is exactly
comap (lowerFactorMap n) inferInstance ≤ lowerRankAlgebra nplus the eventwise mod-null converse. No raw equality is asserted or supplied by this construction; the available converse is eventwise moduloM.law. Nothing here shows the two σ-algebras are unequal — the point is that this argument does not produce an equality, and phrasing the converse as an equality "modulo null sets" would commit to atrim/completionidentification that is not available.Gates:
lake buildclean (3362 jobs), zero sorries, axiom audit 210 → 227 (four commits on the branch), documentation drift checks pass.#107 remains open.