[RemyDegenne]

Dependency sync, outside a Lean release: Tau Ceti and Mathlib move to Tau Ceti's current main, and LML moves to a commit on the same Mathlib that requires Statlib. The toolchain stays v4.36.0-rc2.

Roadmap: none

Pins

Package	Old	New
TauCeti	e0610cc (tag v4.36.0-rc2)	4d91513 (main, CI green, prebuilt files published)
mathlib	1b1ccf4	2ddf59c (Tau Ceti's pin)
LeanMachineLearning	efbe5d2	86a0ab0 (main, the merge of LeanMachineLearning/LML#298)
Statlib (through LML)	none	af34969

Batteries and import-graph move with Mathlib, to Tau Ceti's pins. subverso stays at Verso's 892d6dc.

Repairs

• Mathlib: the EventuallyEqSet/EventuallySubset refactor ([Merged by Bors] - refactor: change the definition of EventuallyEqSet leanprover-community/mathlib4#45712), the enorm → eNorm and nnnorm → nnNorm renames, Submodule.isClosed_of_finiteDimensional, FiniteDimensional.completeSpace, and one section variable no longer used. I listed every deprecation added between the two Mathlib pins and fixed every use of them in LMLExplore.
• Tau Ceti: TauCeti.MeasureTheory.Measure.TotalVariation and TauCeti.Probability.Kernel.Matrix became directories (their Basic files are now imported). TauCeti.Probability.measurable_bernoulliMeasure is now Measurable.bernoulliMeasure, and TauCeti.lowerSemicontinuous_iInf_of_compactSpace is now LowerSemicontinuous.iInf_of_compactSpace. TauCeti.MeasureTheory.map_withDensity_abs_deriv_mul no longer takes a measurability hypothesis (its use in ExponentialFamily/Bernoulli.lean drops it). I checked every Tau Ceti declaration removed between the two pins against LMLExplore.
• LML: its ChainRule, Convex and kernel MeasurableSpace modules moved to Statlib. The two LMLExplore files that imported ChainRule now import Statlib's, and KullbackLeibler/Bernoulli.lean imports Statlib.Divergence.KullbackLeibler.Basic for ProbabilityTheory.klDiv_smul_add_smul_le instead of LML's Convex. DivergenceDecomposition uses Statlib's measurable_klDiv and condKL_eq_lintegral.

Removed declarations

The axioms audit found two duplicates with the new dependencies:

Removed	Replacement
EReal.toENNReal_inv, with its module LMLExplore.Data.EReal.Inv	EReal.toENNReal_inv in Statlib.ForMathlib.EReal
ProbabilityTheory.Kernel.Invariant.pow	the same name in TauCeti.Probability.Kernel.Composition.Power, which LMLExplore.Probability.Kernel.Composition.Comp now imports

Human-owned changes (second commit)

• tauceti.toml: an [[upstreams]] entry for Statlib (update = false, overlap = true, upstream_destination = false).
• AGENTS.md (.claude/CLAUDE.md), README.md, scripts/overlap/, ci.yml and referee-site.yml: Statlib is listed with the other dependencies.
• README.md, lakefile.toml and tauceti.toml: new sync policy, for a maintainer to confirm. Tau Ceti is pinned at a main commit whose prebuilt files are published (usually its release tag), instead of only at Lean releases that both Tau Ceti and LML have tagged. LML is pinned at a commit on the same Mathlib, and Statlib at the commit LML pins.

Checks run locally

Rebased onto main at d4a9f81, after the LML pin moved to the merge commit:

• scripts/build.sh --iofail passes, so no warnings anywhere, dependencies included.
• lake exe axioms passes: no duplicate declarations across 343 LMLExplore modules and 5571 dependency modules, and every axiom is within the allowlist.
• lake exe module-system passes.
• #lint in LMLExplore passes over all modules.

As for every sync, PR CI cannot build this change (the lakefile and pins change), so it needs an admin merge.

After the merge

Run the overlap scan. Statlib has no previous pin, so pass --old Statlib=02a43cdf8d9cbdeaf82e2062d8556476baab22bb (its first commit). Known overlaps for it to report:

• Tau Ceti's Kernel/Composition/Power.lean also has the Markov and s-finite instances for powers and one_def (Comp.lean's one_eq_id).
• Statlib has lintegral_bernoulliMeasure and bernoulliMeasure_absolutelyContinuous (LMLExplore's version of the latter is more general).

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo