The lower-rank conditioning algebra (#107) - #156
Merged
Conversation
Route-independent extraction of `Graphon/RelRankAlgebra.lean`, built from fresh master rather than rebased, so no route-specific work comes with it. `lowerRankAlgebra n = ⨆ A, ⨆ (_ : A.card < n), fixingAlgebra A`, with: * the order API — `_le`, `_mono`, `fixingAlgebra_le_lowerRankAlgebra`; * `lowerRankAlgebra_zero = ⊥` and `lowerRankAlgebra_one = invariantAlgebra`, the latter being the recursion's base case and the reason no `NoNullary` hypothesis is needed: whatever global information the law carries lives in that factor; * `comap_relabel_lowerRankAlgebra` — invariance under an **arbitrary** sortwise permutation family under finitely many sorts. The generality is load-bearing: relabelings that displace infinitely many vertices arise naturally in the polling arguments this factor exists for, and the finite-support transport is unavailable for them. The proof needs only that each `σ s` is an `Equiv`; * `card_inter_lt_of_ne` — distinct supports of equal rank meet in strictly lower rank. Law-free throughout: order theory and one transport lemma, nothing about any measure. All polling, tail, shift, and swap declarations stay on the parked `r4-rank-algebra` branch. The docstring justifying the arbitrary-permutation hypothesis was reworded so it no longer names declarations absent from this branch. Audit 236 → 243. Full build 3361 jobs green; census, axiom audit, and documentation drift checks pass.
The header named the finite-family form of Austin's Proposition 3.12 as "the engine". That is more route-specific than this PR claims: the current design leaves the downstream argument open to the augmented Kallenberg-style rank induction, and this file is route-independent order theory. Reworded to say the missing finite-family statement is *analogous* to Proposition 3.12 and that its proof belongs to the downstream coupling/induction layer, deliberately not fixed here. Prose only. Build green; drift checks pass.
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.
Route-independent extraction, built from fresh master rather than rebased, so no route-specific work comes along. #107 remains open.
lowerRankAlgebra n = ⨆ A, ⨆ (_ : A.card < n), fixingAlgebra A, with:_le,_mono,fixingAlgebra_le_lowerRankAlgebra;lowerRankAlgebra_zero = ⊥andlowerRankAlgebra_one = invariantAlgebra. The second is the recursion's base case and the reason noNoNullaryhypothesis is needed: whatever global information the law carries lives in that factor;comap_relabel_lowerRankAlgebra— invariance under an arbitrary sortwise permutation family under finitely many sorts. This generality is load-bearing rather than cosmetic: relabelings displacing infinitely many vertices arise naturally in the polling arguments the factor exists for, and the finite-support transport is unavailable for them. The proof needs only that eachσ sis anEquiv;card_inter_lt_of_ne— distinct supports of equal rank meet in strictly lower rank.Law-free throughout: order theory plus one transport lemma, nothing about any measure.
Scope
Every polling, tail, shift, and swap declaration stays on the parked
r4-rank-algebrabranch. The only edit relative to that branch is prose: the docstring justifying the arbitrary-permutation hypothesis no longer names declarations absent here.This lands the piece the rank-induction reframing needs —
lowerFactorMapwill be specified againstlowerRankAlgebra— without committing to any particular route through the remaining mathematics.Gates
Full build 3361 jobs green; zero sorries; audit 236 → 243, all new declarations
[propext, Classical.choice, Quot.sound]-clean; documentation drift checks pass.