For an infinite sequence on a standard Borel space, the law is exchangeable if and only if it is a mixture of i.i.d. laws.
These are two descriptions of the same laws. The “directing random measure” ν was implicit on the left: each route builds it from the sequence’s own conditional law, given the σ-algebra that route produces.
Exchangeability: permutation invariance
Every finite-dimensional law is invariant under permuting its coordinates.
Route A proves the hard direction for arbitrary standard Borel α; Routes B and C are formalized for real-valued square-integrable sequences.
Here ConditionallyIID is the mixture identity: it constrains the law of each block, not the joint law of the block with ν. TauCeti later renamed that shape MixedIID.
Contractability, exchangeability and the mixture representation are therefore equivalent. Exchangeable ⇒ contractable is one line: an increasing selection is injective, and exchangeability gives injective selections the prefix law.
Why the formalization grew
≈2.5 pp.
Kallenberg
three compact proofs
→formal interfaces
42,745 LOC
ITP artifact
112 files · 783 declarations
Largely transitive dependencies, plus the mathematics the textbook leaves invisible. The lines are bridge lemmas, route-specific infrastructure, and adapters around Mathlib’s probability APIs: kernels, conditional expectation, conditional independence, tail σ-algebras, product-measure uniqueness, and L¹/L² transport.
Each textbook proof leans on a different slice of measure theory; each slice had to be built or connected to Mathlib before the route could close.
Two subsequent refactorings: paper review (slide 11), then rebuilding a route in TauCeti (slides 12–13).
All three proofs target the same factorization theorem
reverse martingales
L² / CDF
Koopman / ergodic
↘↓↙
a.e., for all selections k₀ < ⋯ < km−1
A block is a finite selection of coordinates; is whatever sub-σ-algebra the route produces: the process tail for A, the σ-algebra generated by the rational-cut limits for B, and the a.e. shift-invariant σ-algebra for C.
from any routeconditional factorizationfor every finite block and measurable rectangle
→
constructrandom measure νωmeasurable, from the one-coordinate conditional law
→
finite-block mixture representation
We fixed this interface before completing the three routes: all three developments were required to prove the same factorization theorem, so measurability and kernel packaging are proved once, and route-specific assumptions cannot leak silently.
Paper Figure 2; the kernel-construction step is detailed in the appendix.
A
Reverse martingales: from the future to the tail
is the future from time m; the process tail is the intersection of them all.
contractabilityfinite-level factorizationhead coordinates exchange against a common future 𝒯ₘ
→ Lévy downward
limittail-level factorizationthe common ending with 𝒢 = 𝒯
Formal bottleneck: the convergence theorem is real-valued; the final theorem concerns arbitrary measurable events in a standard Borel space. The Lean work is transporting real conditional expectations of indicators back to set-level statements.
B
The L² route: empirical cuts to a random law
Here each coordinate is real-valued with . Contractability bounds then make these Cesàro averages Cauchy in L², one rational cut at a time.
rational cut limitscountably many L¹/L² limits
→
measurable conditional CDFmonotone, normalized, right-continuous in q; measurable in ω
→
Stieltjes probability measure νω
Formal bottleneck: turning countably many L¹/L² limits into one measurable random probability measure. The limit object does not come packaged; it has to be rebuilt as a kernel.
C
The Koopman route: projection to conditional expectation
path spacethe shift S preserves the path law; Uf = f ∘ S on L²
→
mean ergodic theoremMathlib gives the orthogonal projection onto Fix(U)
→
conditional expectation given 𝓘then finite indicator factorization
Formal bottleneck: identifying an abstract Hilbert-space projection with the conditional expectation needed by the common ending, over the a.e. shift-invariant σ-algebra, in the measurable form consumed downstream.
Each proof has a different formal bottleneck
A · transport problem
Real-valued reverse-martingale convergence must be transported back to measurable events in an arbitrary standard Borel state space.
standard Borel α · 3,770 route LOC
B · object-construction problem
Elementary estimates produce limits, but the proof still has to construct a measurable random probability law.
ℝ, square-integrable · 12,476 route LOC
C · identification problem
Mean ergodic theory gives a projection; probability needs a conditional expectation and finite indicator factorization.
ℝ, square-integrable · 6,893 route LOC
LOC counts show where each proof needed bridge infrastructure.
How generated proofs were kept on track
The author fixed the statements and decided what to keep; Lean checked what elaborated and compiled; models queried the Mathlib search tools and proposed proofs and refactors.
m ≤ ‹MeasurableSpace Ω› quietly elaborated to m ≤ m→name the ambient m₀ explicitly
the right theorem would not apply: [SigmaFinite (μ.trim hm)] was hidden in the hover→read the signature, then test the application before editing
a proof attempt worked by proposing a different hypothesis→statements are fixed outside the proof loop, and handed back rather than adjusted
Each recurring failure was diagnosed once. The rules and the workflow became lean4-skills:
late 2025Stop the failures that kept recurringWrite down what fixed them; teach the agent to read Lean’s goals, hovers and diagnostics.
early 2026Streamline large developmentsSearch Mathlib before proving, test before editing, stop and report when stuck.
nowEnforce the workflow, keep the human in the loopWhat was searched, what Lean verified, who chose the statement and who signed off.
What changed after review
42,745LOC · ITP artifact
→review + refactoring
26,767LOC · 27 May 2026
local constructions replaced by existing Mathlib APIs;
theorem-facing declarations retained while staging helpers were deleted or made private;
dead wrappers, unused imports, and abandoned proof scaffolding removed.
Declarations fell faster than lines, 894 → 501 against a 37% line cut, because consuming Mathlib left whole helpers with no consumers. Counted the same way in both trees (theorem/lemma/def/instance).
The useful review question was not merely “can this be upstreamed?” but “what should be deleted or replaced first?”
Rebuilding the martingale route in TauCeti
Original repository
TauCeti
completed proof development
dependency-ordered library
source of proof scripts
source of evidence and warnings
local API choices
current Mathlib and TauCeti conventions
theorem already proved
every statement reconsidered
The original repository was a migration source, not the mathematical specification. When a route required a different statement than the fixed interface, we had to determine whether the route or the interface was wrong.
martingale route: landedmixed-i.i.d. summit, equivalence facade and path-law mixture representation on main
L² route: partialblock-average machinery landing
Koopman route: partialfixed space and Markov operator landed
local rectangle / π-system proofs → path-law reindexing, IsProjectiveLimit.unique, and Mathlib conditional-independence characterizations
pair law: ~941 lines of source apparatus → a 46-line public reindexing proof
Weaken the theorem boundary
[StandardBorelSpace Ω]→[MeasurableSpace Ω] [IsProbabilityMeasure μ]→[IsFiniteMeasure μ]standard Borel structure stays on the value space α, where the random probability measure lives
Expose the objects, not the staging
public: MixedIID, MixedIIDWith, directingProbabilityMeasure
private: rectangle integrals and product-kernel assembly
It also corrected the specification. The finite-block predicate constrains only the marginal law of the block, so it was renamed MixedIID; the stronger joint-law ConditionallyIID landed as a separate definition on 26 July, and the theorem concluding it is still open.
Migration re-derived the library against current APIs rather than preserving the proof architecture. Every file the theorem imports: 9,154 → 5,643 lines. Declarations rose instead of falling: this work built an API rather than deleting dead ones.
Conclusions
Mathematics
Three mechanically checked routes to the same representation. Formalized, each one becomes a different interface problem.
Method
The factorization theorem was fixed before the routes were finished, which kept the three developments modular and comparable.
Library design
The TauCeti rebuild cut the reverse martingale route’s footprint by 38%, weakened its public hypotheses, and separated mixed i.i.d. from genuine conditional i.i.d.
Statistics: the artifact table, the common ending as a kernel construction
Routes: finite-to-tail, the CDF bridge, the operator interface
TauCeti: roadmap status, architecture, library design, MixedIID vs ConditionallyIID, current facade
Review: what ten independent angles found, and two conflicts
Paper artifact: codebase statistics
Component
Lines
Files
Declarations
Route-specific
Route A (ViaMartingale)
3,770
13
112
Route B (ViaL2)
12,476
12
96
Route C (ViaKoopman)
6,893
18
138
Shared infrastructure
Common ending & bridge
917
2
29
Theorem files (API)
603
4
15
Probability bridges
10,133
36
156
Ergodic theory
1,959
6
59
Tail σ-algebras
1,214
3
21
Core symmetry API
1,536
3
68
Other helpers / utilities / path space
4,011
15
89
Total
42,745
112
783
ITP paper, Table 1, as published: 42,745 lines, 112 files, 783 declarations (theorem/lemma/def/instance). (Published rows sum to 43,512.)
The common ending is a kernel-construction theorem
Input 1Sub-σ-algebra 𝒢
The conditioning object produced by a route.
Input 2Coordinate conditional laws
ω ↦ μ[X₀ ∈ B | 𝒢](ω), initially as conditional expectations of indicators.
Input 3Finite factorization
Products of indicators factor conditionally for every finite block.
OutputMixedIIDWith μ X ν
A measurable probability-measure-valued mixing representative whose finite product kernels match block laws.
The difficult packaging is from “a family of conditional expectations indexed by measurable sets” to “one measurable random probability measure.”
ARoute A in detail: the finite-to-tail step
Finite future factorization: prove the identity at tailFamily X (m+1) for every m ≥ r.
Lévy downward: conditional expectations converge a.e. along the antitone future family.
Finite products converge: use tendsto_finsetProd on the right-hand side.
Uniqueness of limits: identify the tail-level equality.
Infrastructure built for this route: finite-horizon time reversal (revFiltration), pathwise crossings with uniform expected upcrossing bounds, a.e. limits along antitone families, and the Lévy downward theorem tendsto_ae_condExp_iInf, kept as thin adapters over Mathlib’s forward martingale/upcrossing API.
Mathlib already had many of the abstract CDF/Stieltjes objects.
The local work bridged the particular limits produced by this proof into those APIs and then into the common ending.
Route B is exploratory infrastructure and the prime refactoring target, against Mathlib’s existing CondCDF / CDFToKernel APIs.
CRoute C in detail: the operator/probability interface
What the mean ergodic theorem gives
An orthogonal-projection statement in a Hilbert space.
What the common ending needs
and finite indicator-product identities
A conditional-expectation statement over the invariant σ-algebra.
Most of the formal work is the proof that these two objects coincide in exactly the measurable form needed downstream.
TauCeti roadmap and current status checked 27 July 2026
0Core definitions and symmetryexchangeability, full exchangeability, contractability, mixed i.i.d., and the joint-law ConditionallyIIDWith with its easy projection (#1211) and the i.i.d. worked example (#1223)
1Product kernels and common endingfinite-block mixture ending done; joint-kernel measurability landed (#1193); conditional common ending remains
2Tails, shifts, invariant σ-algebrastails, shifts, invariant σ-algebras, and the Hewitt–Savage zero-one law (#1199, 26 July)
5Koopman / mean ergodic routefixed space and Markov operator landed (#1103, #1118); route not yet complete
6–7Directing measure, summit, equivalence facademixture-form implication and equivalences on main; infinite-product infrastructure landed (#1216, #1217, #1220) and deFinettiMeasure with the mixture representation landed (#1222, 27 July); the conditional summit and the deFinetti* facade remain
Two examples where TauCeti changed the architecture
Migration source941 LOCPairLawEquality.lean (556) + FutureRectangles.lean (385): explicit reindexing maps, a rectangle π-system with its Dynkin argument, and a hand-built measure-extensionality lemma.
→
TauCeti46 + 20 linesContractable.pairLaw_eq (46) over pathLaw, plus shared reindexing helpers (20). The replaced apparatus served this step alone.
Tower short-circuit at the directing-measure endpoint: the theorem that two coordinates have the same conditional law on the tail now follows from condExp_condExp_of_le (the ordinary tower property) and no longer depends on reverse-martingale convergence.
Reverse martingales remain necessary for tail factorization: passing finite products from future σ-algebras down to the tail still consumes Lévy downward.
thin adapters over Mathlib upcrossing and convergence APIs
Hypotheses:IsProbabilityMeasure → IsFiniteMeasure wherever μ univ = 1 was unused; StandardBorelSpace Ω → MeasurableSpace Ω for the public existential statements, via path-law transfer; standard Borel stays on α.
Visibility: public MixedIIDWith/MixedIID/directingProbabilityMeasure with characteristic simp lemmas; rectangle-mixture staging private and colocated with its consumers.
Pruning: dead futureFiltration (#813/#822), duplicate indicator helpers (#557), unused corollaries (#835), vestigial case splits (#621), and unnecessary public imports throughout.
MixedIID is not ConditionallyIID
Both range over all finite selections k₀ < ⋯ < km−1. The first equation constrains only the marginal law of the selected block: on a sufficiently rich space, an independent random measure with the same mixing law can satisfy it without directing X.
TauCeti renamed the first predicate MixedIID (#1192, 25 July). The second is now the definition of ConditionallyIIDWith on main (#1211, 26 July), which also proves the projection mixedIIDWith_of_conditionallyIIDWith. The arrow runs one way only; the theorem concluding the conditional form from contractability is still open.
The finite-block theorem was correct; its original name promised a stronger coupling statement.
TauCeti PR #1192, 25 July 2026; main ships the mixture equivalences under the new names, with no deFinetti* aliases.
Current TauCeti facade and remaining roadmap
TauCeti/Probability/DeFinetti/Theorem.leancurrent main
theoremexchangeable_iff_mixedIID … :
Exchangeable μ X ↔ MixedIID μ X
theoremcontractable_iff_mixedIID … :
Contractable μ X ↔ MixedIID μ X
nextUniqueness of the mixing lawcompact-box multivariate moment determinacy, then injectivity of π ↦ π.bind (P ↦ P⊗ℕ), then mixedIID_mixingLaw_unique. The first two are pure measure theory; #1222 deliberately left the corollary out.
thenThe conditional chainconditionallyIID_of_jointRectangles (the Layer 1 conditional common ending), then the summit conditionallyIID_of_contractable / _of_exchangeable, then conditionallyIID_ae_unique. This is what restores the deFinetti* names.
afterThe rest of the representationdeFinetti_mixture, which derives a directing measure instead of assuming one; deFinetti_empiricalMeasure in the weak topology on ProbabilityMeasure α; exchangeable_extreme_iff_iid, which has its Hewitt–Savage input from #1199 but still needs the mixture theorem.
openThe other two routes, and later symmetrydeFinetti_viaL2 (the L² library landed, the route to de Finetti did not) and deFinetti_viaKoopman (only FixedSpace and KoopmanMarkov groundwork; the mean-ergodic projection and proj_eq_condexp are missing); then aggregators, worked examples, arrays and Markov exchangeability.
The deFinetti* handles are vacant by design. #1192 retired deFinetti, deFinetti_equivalence and deFinetti_RyllNardzewski_equivalence, the last of which is the paper’s headline theorem on slide 3; the conditional summit is what earns them back.
Idiomatic, conclusion-shaped primary names (conditionallyIID_of_exchangeable, not deFinetti). A roadmap alias survives only while it stays semantically faithful: #1192 retired the deFinetti* aliases rather than let them name a mixture-only statement.
Pattern 2 · visibilitySharing constrains privacy
Extract public API only for cross-file consumers; colocate a private core otherwise; delete wrappers that duplicate Mathlib.
Pattern 3 · hypothesesRefactor to dissolve generality/correctness conflicts
Split statements or restructure proofs so every hypothesis is genuinely load-bearing.
One round required a characteristic lemma such as foo_apply; the next requested removing @[expose]. lake env lean then failed: the lemma was no longer definitionally provable.
Resolution: keep exposure. A reproducible compiler failure beats an aesthetic assertion (#451, #612, #666).
Contest-and-link: quote the opposing finding and show the contradiction explicitly.
Naming governs primary names. Keep a roadmap handle as an alias only when it does not promise a stronger proposition.
Share reasoning at the right visibility: public, private, or delete if Mathlib owns it.
Refactor to satisfy both rubrics: split statements, relocate consumers, make hypotheses load-bearing.