chore(bump): mathlib 8acb872c311a (2026-09-01) — BLOCKED on verification gate, do not merge

[CBirkbeck]

Daily mathlib bump. Do not merge yet — the verification gate is blocked, see the bottom.

pin	e4b72ca0d01c → 8acb872c311a (259 commits)
toolchain	v4.34.0-rc2, unchanged — pin-only bump
batteries	d54dddc5 → 7e23602c
freeze	#8576 (deliberately left open)
escalation	bead am-waf, .mathlib-quality/bump-escalation.md

Two hard breaks, both fixed — no statement changed

1. mathlib#39703 "create a Basic top folder" moved Mathlib/Logic/Denumerable.lean to
Mathlib/Basic/Denumerable.lean with no shim module, so the old path stops resolving. One
import, in LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/Foundation.lean.

No name changed, so every declaration-name screen misses this. It was caught by comparing all
1 097 Mathlib.* modules we import against the 8 466 in the new Mathlib.lean — exactly one
had gone missing.

2. Ideal.absNorm swapped [Module.Free ℤ S] for [Infinite S] (AbsNorm.lean, variable [Infinite S]). No rename, no alias, no warning — just a synthesis failure. Proven rather than
guessed, by reproducing our own binder pattern against the new mathlib:

example {R : Type*} [CommRing R] [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R]
    (I : Ideal R) : ℕ := Ideal.absNorm I
-- failed to synthesize instance of type class  Infinite R

We touch absNorm in 86 files, which looked alarming. A probe bounded it: uses over 𝓞 K are
covered by the global CharZero.infinite, so only lemmas stated for a generic ring carrying
[Module.Free ℤ R] lose the instance — 4 files.

absNorm occurs in those statements, so a haveI in the proof is too late, and adding
[Infinite R] to the binders would be a statement change, which a bump may not make. Upstream hit
the same wall and deliberately did not add a global instance — it declares the bridge local at
each use site (AbsNorm.lean:355, RelNorm.lean:456-457, FractionalIdeal/Norm.lean:43). Same
idiom adopted here, so all four files keep their statements byte-identical.

Three deprecation renames (warning-level), adapted

IsTopologicalRing.to_topologicalAddGroup → .isTopologicalAddGroup and
IsModuleTopology.topologicalAddGroup → .isTopologicalAddGroup (mathlib#43027, 51 sites), and
PowerSeries.deriv_log → .derivative_log (2 sites). All keep live aliases with identical binder
order, so these only warned. The deriv_log rewrite was word-bounded — our own
deriv_log_mul_one_add_X and subst_deriv_log_mul_one_add share the prefix and are untouched.

Verified

LocalizationTopology.lean elaborates with zero errors (it was the site of the confirmed #43027
warning); DirichletBounds.lean clean; the absNorm repair reproduced on the real two_le_absNorm
statement; Foundation.lean elaborating with no errors reported. Evidence in
.mathlib-quality/bump-lsp.json, method and per-finding reasoning in bump-changelog.md.

Why this is not ready to merge

AINTLIB has no build CI. check-runs for this head returns total_count: 0, main has no
branch protection, and the only workflows are the Blueprint Pages ones (failing since 2026-06-24).
The verify-full-build step is explicit: if the branch has no CI path, stop and escalate; never
substitute a local build. So no local build was run and nothing is merged.

Four files elaborated locally shows the known breaks are fixed. It is not a green build over
~3 500 modules — signature, simp-set and instance-resolution changes only surface under full
elaboration. A decision is needed (add CI / grant a one-time local-build exemption and fix
bump-build-green.sh / re-scope the worker); see bead am-waf.

🤖 Generated with Claude Code