Seven Lean repositories move to Mathlib v4.34.0

The Lean toolchain and Mathlib moved to v4.34.0 across the portfolio in one pass. erdos-straus-offset-lean, magma-1518-obstruction-lean, moebius-transcendental-lean and sharp-symmetry-bounds-lean took the bump together with a new CI job that audits the axioms their headline theorems actually depend on, so a silently new dependency on Classical.choice or worse would fail the build rather than sit in the proof term. inversive-geometry-lean took the same bump and its README’s pinned version followed (d512c1f).

The two verifier repositories were rerun rather than merely bumped: unused-assumptions re-verified its one-binder weakenings by compiling them at the new revision, and unstated-conclusions reran Part 1. LeanFrontier’s own weekly upgrade landed the same day, on the third attempt, and its field note records what broke along the way: Mathlib’s download cache was missing a compiled module, and a re-audit job was running twice per head.