Bump to Lean v4.33.0 / Mathlib v4.33.0

[jeremy-kahn-brown-ai]

Jeremy Kahn asked me to prepare and submit this PR; it was written by Claude (an AI assistant) working under his direction, and he takes responsibility for it. Context: his group is starting a formalization of progress toward MLC (local connectivity of the Mandelbrot set) that builds on this repo's Böttcher/potential/parameter-map results, and wanted ray on the latest stable toolchain first.

What this is

A port from Lean v4.27.0-rc1 / Mathlib master@2025-12-29 to Lean v4.33.0 / Mathlib v4.33.0 (latest stable release). 68 files, +1312/−572. No mathematical content changed; the module system (module/public/@[expose]) is untouched. The branch mathlib-v4.33.0-waves has the same changes split into 8 stepwise commits with a per-file changelog, if that's easier to review.

Highlights

• TangentSpace is no longer reducible in Mathlib, which broke the pervasive TangentSpace I z = ℂ defeq usage (~10 files). Rather than set_option backward.isDefEq.respectTransparency false (which Mathlib uses internally for this, but which is a transitional option), the port adds two @[expose] identity bridges tangentToC/tangentOfC in Ray/Manifold/OneDimension.lean and restructures proofs to cross the TangentSpace/ℂ boundary at explicit points. Statements unchanged.
• Deleted lemmas that now exist in Mathlib with compatible statements (checked before deleting): flip_flip, ContinuousLinearMap.smulRight_zero, AnalyticAt.div_const, Circle.coe_neg + the local Circle negation instances (Circle.neg_def kept and reproved against Mathlib's instance).
• Renames forced by upstream: limUnder → Filter.limUnder, EMetric.ball → Metric.eball, NoAtoms → NullSingletonClass, and Directed Superset → Directed (· ⊇ ·) in IsPreconnected.directed_iInter (Set's HasSubset-based spelling no longer elaborates; logically equivalent).
• Stream'/ℕ → X mixed terms are now rejected at implicit transparency: handled with fully Stream'-typed helper lemmas. HasDerivAtFilter's new formulation: bottcher_hasDerivAt_one reproved via hasDerivAt_iff_isLittleO with the same estimates. Repo-wide deprecation sweep (zero deprecation warnings remain).
• Small new public helpers: push_sum_get/push_prod_get, sum_cons_get/product_cons_get/product_drop_get, tangentToC/tangentOfC.

One deliberate lakefile change to flag

require mathlib @ git "master" → @ git "v4.33.0", pinning the release the port was verified against. Happy to revert that line to master if you prefer tracking it — the source fixes themselves are what matters.

Verification

• lake build green (3,301 jobs), zero sorry, zero deprecation warnings.
• #print axioms isConnected_mandelbrot = [propext, Classical.choice, Quot.sound].
• No set_option maxHeartbeats raises, no backward.* options, no native_decide introduced.

We're glad to adjust anything — split differently, rename the bridges, drop the pin change, or rebase onto a newer target.

🤖 Generated with Claude Code

https://claude.ai/code/session_01SKTPd9aJaVimWs9EW5zXnY

[girving]

Can you remove the build.log files? Might want to add something to gitignore to prevent that mistake in future.

[girving]

Otherwise looks great, thank you!

[jeremy-kahn-brown-ai]

Done — removed both build logs from the PR branch (amended, so it stays a single clean commit) and added *.log to .gitignore. The mathlib-v4.33.0-waves reference branch got the same cleanup as a follow-up commit. Thanks for the review!

🤖 Generated with Claude Code

https://claude.ai/code/session_01SKTPd9aJaVimWs9EW5zXnY

[girving]

Great, merging. But in future making it be a separate commit is better, so that during review I can see the deltas between commits that I've reviewed.