Extract the shared polling infrastructure (#107) - #155
Merged
Conversation
The tail engine and its two companions were `private` in `RelFixingCondIndep`. The rankwise relative-independence argument is their second real consumer, so they move to `Graphon/RelPollingInfrastructure.lean` rather than being duplicated. Public, and the whole intended interface: * `condExp_ae_eq_condExp_of_comap_eq` — the tail engine; * `InfiniteRelExchangeableLaw.measurePreserving_relabel`; * `InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra`. The `L²` squeeze and `condExp_comp_of_measurePreserving` stay private inside the new module: they are the proof of the tail engine, not part of its interface. The two law-dependent declarations are renamed into the `InfiniteRelExchangeableLaw` namespace, so call sites read `M.measurePreserving_relabel` and `M.relabel_preimage_ae_eq_of_fixingAlgebra`. `RelFixingCondIndep` imports the new module and its copies are deleted; it keeps its single public headline `condIndep_fixingAlgebra`. The three extracted declarations are now audited in their own right, which they were not while private. Audit 203 → 206. Full build 3360 jobs green; census, axiom audit, and documentation 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.
Prerequisite refactor before the rankwise relative-independence work. #107 remains open.
The tail engine and its two companions were
privateinRelFixingCondIndep. The rankwise argument is their second real consumer, so they move to a shared module rather than being duplicated.New
Graphon/RelPollingInfrastructure.leanexposes exactly three declarations:condExp_ae_eq_condExp_of_comap_eq— the tail engine: a measure-preservingTthat fixesfa.e. and pulls the conditioning algebram₁back to a sub-algebram₂ ≤ m₁forcesμ[f|m₁] =ᵐ[μ] μ[f|m₂];InfiniteRelExchangeableLaw.measurePreserving_relabel;InfiniteRelExchangeableLaw.relabel_preimage_ae_eq_of_fixingAlgebra.The
L²squeeze andcondExp_comp_of_measurePreservingstay private inside the new module — they are the proof of the tail engine, not part of its interface.The two law-dependent declarations are renamed into the
InfiniteRelExchangeableLawnamespace, so call sites readM.measurePreserving_relabelandM.relabel_preimage_ae_eq_of_fixingAlgebra.RelFixingCondIndepimports the new module and its copies are deleted, preserving its single-public-headline claim while making the reused infrastructure explicit. A side benefit: the three extracted declarations are now audited in their own right, which they could not be while private.No mathematical content changes. Full build 3360 jobs green; zero sorries; audit 200 to 203; documentation drift checks pass.
Correction. The commit message on
c075d36says "203 → 206". That is wrong: the audited-declaration count goes 200 → 203. My earlier figures came fromgrep -c "print axioms", which also matches prose lines in the file header. The authoritative counts aregrep -c '^#print axioms ' scripts/axiom_audit.leanandlen(AUDITED_DECLS), both of which give 200 on master and 203 on this head. Counts quoted in some earlier PR bodies in this series are inflated for the same reason; the enforced lists themselves have always been in sync, since the gate compares the printed set against the intended set directly rather than by count.