Bump to Lean v4.33.0-rc1 / Mathlib 0434c033 / BrownianMotion 314f04a, and consume what upstream now provides

[raphaelrrcoelho]

Three commits: the pin bump, the upstream-consumption pass it unlocked, and the README pin row.

The bump (1819f4f)

Matches BrownianMotion's own dependency set exactly — BM's head pins Mathlib 0434c033 on v4.33.0-rc1, and lake update resolves aesop/batteries/Cli/Qq/proofwidgets to BM's revs. This is a Lean release candidate. Stable v4.33.0/v4.33.1 exist, but BM never moved to a stable v4.33.x, so taking one would strand it. The README pin row now says so.

PR #168 declined this same bump because BM's head "would strand LeanArchitect (no v4.33.0 tag)". That reason has expired — hanwenzhu/LeanArchitect now tags v4.33.0-rc1, v4.33.0, v4.33.0-rc2, v4.34.0-rc1 — so it was re-derived rather than inherited.

Six source changes were forced. Every one is a type or normal-form change underneath a name that still exists, which is the class no name-level sweep can see:

• BM relocated Function.IsRightContinuous (Mathlib now has a Filtration.IsRightContinuous of the same name) → _root_.IsRightContinuous, 7 sites. This alone was 11 of the original 27 errors.
• Finset.lt_inf'_iff became to_dual-generated from sup'_lt_iff with the nonemptiness proof explicit, so it no longer fires under simp/rw → (Finset.lt_inf'_iff _).2, as Mathlib's own call sites now do.
• WithTop coercion normal form → not_le ahead of coe_lt_coe, 3 sites.
• LinearIsometry.norm_map stopped matching as a rewrite against the coercion head → applied as a term.
• A Decidable instance mismatch left a goal of the form X = X that rfl cannot close → congr 1.
• NNReal.coe_mk stopped firing → show, for the defeq.

Plus 16 explicit uses of names the new Mathlib deprecates (Set.setOf_* to Set.ofPred_*, ENat.coe_le_coe to ENat.natCast_le_natCast). The residual deprecation warnings come from Mathlib's own default simp set, not ours.

The consumption pass (02fac19) — 28 files, −141 net lines

A four-agent survey read all 140 Foundations/ modules against the pinned sources. Every consumption below was confirmed by reading the upstream statement first.

• predictableRect restated, definition for definition, what BM now ships as Filtration.predictableRectangles (#506). Our 54-line IsPiSystem proof is one projection of BM's strictly stronger isSetSemiring_predictableRectangles (#517). Three non-obvious costs: it needed an explicit public import (transitively available is not visible to importers), BM binds the Ioc existential in a different order, and BM's bot piece is {⊥} where ours wrote {(0 : ℝ≥0)} — defeq but not syntactically equal, which silently broke two rewrites.
• tendstoInMeasure_congr_left deleted. Its docstring claimed "a generic congruence Mathlib does not ship in this left-argument form"; TendstoInMeasure.congr has exactly our ∀ i hypothesis shape. All four call sites consume upstream directly, so no wrapper is left behind. docs/values-review.md had filed this lemma twice as wanting a "Mathlib-shaped home" — upstream built it.
• isCadlag_of_continuous deleted from all three files that had it, two of them documenting the duplication as deliberate ("B3's is private; re-derived"). BM's Continuous.isCadlag is the same lemma on a weaker typeclass.

Nine false or stale prose claims corrected. These matter more than the line count, because each one was actively hiding work:

• ConvexDuality claimed the bundled cone types were unavailable "at this pin". That docstring is what kept a re-derivation of Farkas invisible: Mathlib ships ProperCone.hyperplane_separation.
• SuperhedgingDuality blamed "a polyhedral / Farkas fact not available in Mathlib". Farkas is available; the blocker is one missing lemma, closedness of a finitely generated cone. That changes the follow-up's cost estimate.
• OptionalSamplingInequality asserted BM's sibling "is a sorry stub at the current pin" and pitched ours as an upstream donation. BM proves it now, and more generally on four axes.
• Girsanov said gir-thm-9.1.8 "remains open" — it is full — and wrote the drift correction with the wrong sign.
• GirsanovConstantTheta said the bounded-adapted case "remains open"; three files deliver it. ItoIntegralProcess listed four deferred items that all ship. ItoIntegralAgainstMartingale and PointwiseBracket disclaimed results downstream files now provide — the understating direction. ExpMin's header claimed the minimum of independent exponentials has Exp(sum rates) where the file proves the survival function. And isPiSystem_predictableRect's docstring still narrated the four-case hand proof deleted in the same commit.

Seven dead declarations removed, one of which a 2026-05-29 review had explicitly flagged "for trim if no consumer appears" — none appeared. rectTerm_eq_elemIntegrand was additionally a theorem that was its own definition unfolded.

Recorded so no future session pays for it twice: BM's predQuadVariation routes through a sorry-backed IsLocalSubmartingale.doob_meyer, so the pathwise quadratic-variation backlog is not closable by upstream consumption at this pin; BM's continuous-time martingale convergence is stubbed; its uniformIntegrable_of_eLpNorm_le requires q < p strictly and so misses our q = p case; and BM has stubbed the Doob L^p maximal inequality we prove in full, which is a better donation target than the optional-sampling one we had been claiming.

Gap claims re-tested and still true, so their docstrings stand: Gamma/Erlang convolution, Poisson moments, probit and the Gaussian CDF, Riemann sums, the L^p-bound-to-uniform-integrability producer, the TendstoInMeasure algebra, Poisson thinning, the space-time SimpleProcess, matrix tanh, and the L2 martingale convergence theorem.

Verification

lake build MathFin green (9210 jobs) and lake lint clean, in the pinned container, on the final tree.

The ledger is stale by construction. The pins sit in every entry's input hash, so all 372 rows restale — which is exactly the circularity pin-bump.yml and ledger-sweep.yml were built for. The intended sequence applies: this PR touches pin files, so the sweep runs its twelve --exec shards and commits the refreshed ledger back to the branch, and build.yml stays red until it does. Do not merge on the pin-bump build alone — a green pin-bump run is the narrower claim that there is something worth verifying, not that the corpus is verified.