chore: bump Lean and Mathlib to v4.35.0-rc3

[github-actions]

Upgrade Lean and Mathlib to v4.35.0-rc3 and port the affected proof code without weakening theorem statements.

The compatibility changes update renamed APIs, parser-sensitive expressions and inference, preserve the four-layer Pauli reachability conclusion, and explicitly select the intended constructors. The follow-up repair also replaces deprecated multi-location rwa syntax, states the intended universe-zero singular functors, and gives accurate migration guidance for dhyp without changing its explicit-argument API. Main has been merged through da8a453; its registry and generated root index are preserved byte-for-byte.

Validation at ed5fefc:

• Independent source review found no theorem weakening or removed declarations in the inspected compatibility changes. All 1,594 textual declaration signatures across the 27 follow-up repair files are unchanged.
• The same universe annotations are applied to nine matching calls in four downstream files, all with explicitly universe-zero spaces. The unchanged static header, forbidden-source, file-size and proof-size checks pass on all 31 repaired files; git diff --check passes.
• The original CI run compiled seven failing shards successfully before rejecting warnings; one shard had four universe-inference failures in SingularMayerVietoris, one shard passed, and shard 00 remained running when the follow-up was pushed. The repair targets the concrete diagnostics, not a blanket linter suppression.
• Fresh full CI: https://github.com/Vilin97/lean-pool/actions/runs/36177693486. Compilation, style, full lint/quality/trust checks and challenge verification are pending. No local rc3 compilation is claimed: this VM has no matching toolchain/dependency cache.

Keep this PR draft until the fresh required checks pass and review is complete. No workflow, gate, linter setting or waiver was changed by the follow-up repair.

[Vilin97]

Provisional review of exact head 38fc74750047e8b0fa5a5f4174ca9ff038aab583: source changes are suitable for CI validation, but this draft is not yet ready to merge.

I inspected the compatibility diff and checked the significant statement changes explicitly: the quadratic pairing range uses the same additive-hom range with its domain specified; the Pauli witness still proves the same four-layer conclusion using idle-layer monotonicity; and the ZFInt order result keeps its statement. No mathematical weakening or deleted declaration was found in the inspected port. The follow-up repair preserves all 1,594 textual declaration signatures in its 27 files and replaces only diagnosed APIs, constructor selection and proof elaboration syntax. The four singular functor calls now fix the universes already required by their Type-valued spaces. The dhyp deprecation now explains the explicit-to-implicit argument migration while preserving its API.

The concrete old-run evidence was 56 warning diagnostics across the completed shards (deprecations, ambiguous constructors and a replacement-signature mismatch) plus four universe-inference errors and their four resulting unsolved goals in SingularMayerVietoris. Seven failing shards had completed compilation before failing the warning gate. This supports a bounded compatibility repair, not rejection for a speculative large proof port.

Static header/forbidden-source/size checks pass on the repaired files, and main's registry/index are preserved exactly. Fresh full rc3 CI 36177407406 must validate the proof substitutions and all required gates, particularly the legacy rwa sequencing and singular functor inference. No local rc3 build or completed style/trust audit is claimed. Keep draft pending those results; I will address remaining bounded failures without changing checks or introducing waivers.

[Vilin97]

Follow-up exact-head review for ed5fefce03db164b5cd4afe3cd16f28efd04832f: the prior source assessment still holds. A targeted scan found nine identical singular-functor applications in four downstream Hopf modules that could not be reached until the earlier module compiled. Each surrounding theorem already quantifies its spaces in Type; the same universe-zero instantiation is now explicit there as well. The statements and proof bodies otherwise remain unchanged.

All 31 repair files pass the unchanged static header, forbidden-source and size checks. A second reviewer independently checked the six legacy rwa replacements: WinAsap retains the exact old macro expansion and its outer omega, and the other rewrites preserve their goal sequencing. No local rc3 compilation is claimed.

The current full validation run is 36177693486. Keep draft pending compilation and all required checks; this comment is a provisional source assessment, not a completed gate approval.

[Vilin97]

Source-review update at 0f971229738a7bb1fbdbd856e8a389cd001f4609 (repair 4cdde109d plus lossless integration of main 0e9b057b). Source changes are approved provisionally; this is a COMMENT review because the authenticated account authored the PR.

The follow-up addresses the diagnostics collected from the current-head build run 36177693486: known single-goal rw/assumption sequencing, focused disjunction introduction, harmless line wrapping, the explicit list-length bound in WinAsap.num_le_length, and three manifold chain-rule proof adaptations. In the latter, mfderiv_comp_apply_of_eq explicitly uses the chart inverse identity to identify the evaluation point, and the rc3 mfderiv_eq_fderiv bridge supplies the canonical tangent-space identifications. The mathematical statements and assumptions are unchanged. A scoped source audit found 1376 unchanged existing named declaration headers in the 12 modified Lean files; independent source review covered the proof changes. This is source evidence, not a claim of rc3 elaboration success.

The challenge verifier failed before exporting environments because lean4export was still pinned to v4.34.0. Its pin now follows the official v4.35.0-rc3 tag, 66f1fb4bc256072069767fce52d39480e4524869. The upstream comparison changes only the toolchain and expected test output; exporter implementation, comparator and landrun pins, verification logic, and challenge contracts are unchanged. Primary evidence: official exporter comparison.

The old head finished with six successful shards and four failed shards; all reported failures in those four are covered by this follow-up. Scoped header, forbidden-source, file-size, proof-size, and whitespace checks pass. All 218 current-main cards, generated indexes, and challenge registry are byte-identical to main; incoming source changes were preserved. No local rc3 build or dependency download was performed. Full rc3 build, lint, trust, and challenge verification must pass on the replacement head. The PR remains draft. No gate, linter setting, or waiver was changed.

[Vilin97]

Source review of 8b86edf0824a28702efa077acd7e8083632697a6: the remaining two-file rc3 repair is appropriate, subject to fresh required CI. Keep this PR in draft.

The preceding head failed in Smale2.lean because the pinned Mathlib now places canonical tangent-space maps around fderiv. The repaired proof first establishes invertibility of the manifold derivative using the same chain rule and hcinv.comp hinv, then transports that result through mfderiv_eq_fderiv. The other derivative proof explicitly reduces to t * 1 = t. Core3.lean now uses contMDiffAt_localInverse, the exact replacement for its deprecated alias in pinned Mathlib c55e6e786f49471c72fbddbec5415808896aec1e.

All 275 existing declaration headers in these two files are unchanged. Scoped header, forbidden-text, file-size and proof-size checks pass. Independent source review covered the complete patch. Main 854da85a8bc6c9219c2c04ec9d43d4a49f43aef8 was integrated losslessly: all nine incoming files, all 219 project cards, all three generated indexes, and the challenge/solution trees are byte-identical to main; the reviewed two-file patch is preserved.

No local rc3 compilation or index-generator execution is claimed. Fresh full rc3 build, linter, quality/trust and challenge-verification checks must validate this exact head before acceptance. Gates, linter settings and challenge contracts are unchanged by this follow-up. This is a COMMENT review because the reviewing account also authored the PR.

[Vilin97]

Changes requested by automated review

Reviewed 8b86edf0824a28702efa077acd7e8083632697a6 under the toolchain/refactor rules. The prior complete source review and its preserved theorem contracts still apply, but fresh compilation disproves the earlier repair's sufficiency.

The exact-head shard 08 build fails at LeanPool/HopfProblem/Recognition/Smale2.lean:5264: change t * (1 : ℝ) = t requires an unavailable HMul (TangentSpace 𝓘(ℝ, ℝ) 0) ℝ instance. After mfderiv_eq_fderiv, the introduced tangent vector still crosses the new tangent-space equivalence; it is not definitionally a real scalar. Transport the derivative equality through the canonical equivalence, retaining the existing theorem statement, then obtain warning-free full-shard, linter/trust and comparator success at the resulting head. Do not add an ad hoc multiplication instance or change the checks.

Draft status is not the reason for this disposition; this is a concrete compiler rejection. No new local rc3 compilation is claimed.

[Vilin97]

At 91958e5cbc27f066b6ee62b654354f015c7755fa, the Smale2 scalar derivative proof now explicitly changes the introduced tangent vector's local type to ℝ before elaborating multiplication. The pinned TangentSpace definition is definitionally the model space but deliberately avoids automatic typeclass unfolding. This supplies the type information missing from shard08's HMul (TangentSpace 𝓘(ℝ, ℝ) 0) ℝ error. The existing t * 1 = t proof, theorem contract, and all other tracked files are unchanged.

The previous exact-head run at 8b86edf0824a28702efa077acd7e8083632697a6 passed eight shards and challenge verification; shard08 failed at this line, while shard00 was cancelled before completion. Its available log supplied no further scoped Lean diagnostics. That is not a completed full-pool validation.

The unchanged scoped header, forbidden-text, file-size and proof-size checks and whitespace check pass for this correction. No local rc3 compilation was run. The draft remains open pending fresh required CI, including shard00; no main refresh, gate, option, waiver, card, index, challenge or dependency change is included.

[Vilin97]

Source review and bounded repair at d292eae81507dc30c2e7eed4ca330b3ef0df83a2 (draft remains pending CI).

The previous head's shard 08 failed at HopfProblem/Recognition/Smale3.lean:1216: the reverse mfderiv_eq_fderiv rewrite no longer matches a bare fderiv after Mathlib introduced canonical tangent-space transports. The repaired proof applies the existing vector-valued chain rule and its forward derivative bridge with full definitional transparency.

The same source audit identified 12 downstream reverse-bridge uses in Smale4–8 and Degree2–3. This batch rewrites those uses through the existing chain-rule/forward-bridge APIs, preserving their point equalities, tangent vectors, and invertibility arguments. These downstream edits address the same API change proactively; they are not 12 additional observed CI failures.

Validation: all 2,067 parsed declaration headers in the eight affected files are unchanged; no declaration or non-proof definition was added or removed. All other files, including cards, indexes and challenge contracts, are byte-identical. The four existing scoped source checks and whitespace check pass, and an independent reviewer read the complete patch and relevant pinned Mathlib definitions. No local rc3 compilation was run. At the last check of the prior-head run, eight shards and challenge verification had succeeded, shard 08 had failed, and shard 00 was still running. Fresh current-head compilation and all required CI remain necessary before merge. No gate, option, waiver, or CI queue was changed.

[Vilin97]

Source follow-up at 1856d7337971bcc6b02aea36659f53b4c5318d35: source-approved, with fresh rc3 CI still required. This remains a draft.

The preceding d292eae8 run passed eight build shards and challenge verification. Shard 08 then exposed two remaining Smale6 chain-rule conversions and seven deprecated local-inverse aliases; shard 00 was still building at the last check. Its run was left intact.

The two conversions now use Mathlib's vector-valued mvfderiv_comp/mvfderiv_eq_fderiv, retaining the same differentiability hypotheses and basepoint equalities while avoiding the additional codomain tangent transport. The seven renamed references use the exact replacement declaration behind Mathlib's deprecated alias. All 1,211 declaration headers across these five files are unchanged; no definitions, assumptions, numerical constants, cards, indexes, challenge contracts or gates changed.

Independent source review, whitespace checks and the four scoped source gates passed. No local rc3 compilation was run; these new proof elaborations and the full required checks await fresh CI. No workflow retries or cancellations were performed.

[Vilin97]

{
"summary": "Source follow-up at 0f28917 for the two actual Smale6 errors in shard 08 of run 36222577025. Both chain-rule equalities now use ContinuousLinearMap.ext and the pinned mfderiv_comp_apply_of_eq theorem, supplying g 0 = f 0 and chart(center t) = f p explicitly. This follows the existing Smale1 proof pattern and removes the unused transported differentiability proof. Independent source review passed; all 259 declaration headers and all bytes outside three proof fragments are preserved. Four scoped static checks and git diff --check passed. This approves the bounded source repair, with no local rc3 compilation claim: the draft and required CI remain pending. At publication, the previous head had eight successful build shards, shard 08 failed, and shard 00 was still running; those results do not validate this new head.",
"assessment": {
"scope": "Two proof repairs for the rc3 derivative API",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The explicit pointwise chain rule preserves the existing maps, assumptions and conclusions while avoiding dependent basepoint rewriting; fresh exact-head CI must establish elaboration."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

{
"summary": "Focused source follow-up at d8f76fa for the actual Smale7:4097 failure in shard 08 of run 36225753570. normalDetector_eq_native now applies the continuous-linear-map equality to a vector and uses the pinned mfderiv_comp_apply_of_eq theorem with the existing inverse identity in its forward direction. This keeps the derivative of q at chart(center t), avoids dependent basepoint rewriting, and removes only the unused transported differentiability proof. All 289 declaration headers and every byte outside this private proof fragment are preserved. Independent review of the complete context and pinned API passed; four scoped static checks and git diff --check passed. The previous Smale6 repairs compiled in that actual CI run before it reached this new error, supporting reuse of the same proof pattern. This new six-line replacement has not been compiled locally under rc3. Approval here covers the bounded source repair only: the draft and unchanged PR body are preserved, and fresh required CI remains pending.",
"assessment": {
"scope": "One private chain-rule proof repair for rc3",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The explicit pointwise chain rule preserves the theorem and all maps while eliminating the failing basepoint rewrite; exact-head CI must validate elaboration."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

Focused source repair at 7b37197526df2b1d8751196370e748a53065a595; draft remains pending current-head CI.

The preceding head's shard 08 failure leaves one goal in Recognition/Smale9.lean: canonical source/codomain tangent-space identifications surrounding the continuous linear map L. Three proof lines apply continuous-linear-map extensionality and reflexivity, using the identity forward/inverse functions of the pinned NormedSpace.fromTangentSpace. The normal derivative equation, arc/germ, hypotheses and complete transversality construction are unchanged.

Validation: all 304 textual declaration headers and all bytes outside this insertion are preserved; the project inventory, registry, root index and compiler configuration are unchanged. The four existing scoped source checks and whitespace check pass, and an independent reviewer inspected the full proof context, actual residual goal and pinned definitions. The preceding CI run compiled Smale6, Smale7 and Smale8 successfully before this Smale9 failure; those observations validate the earlier repairs only.

No local rc3 compilation was run for this change. Fresh compilation and every required CI check remain necessary before merge; preserve the draft hold. No checks, options, waivers or CI queue were changed.

[Vilin97]

{
"reviewed_commit": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f",
"conclusion": "The two-file warning repair passes source review and scoped static checks. Fresh exact-head CI remains required; the existing PR lifecycle is preserved.",
"scope": {
"baseline": "7b37197526df2b1d8751196370e748a53065a595",
"files": [
"LeanPool/HopfProblem/Threefold/SpecialPeriods11.lean",
"LeanPool/HopfProblem/Recognition/Smale11.lean"
],
"change": "Replace two deprecated aliases and wrap one proof line; all theorem statements, proof arguments, data and imports are unchanged."
},
"evidence": {
"prior_shard": "At the exact baseline, shard08 completed all 5,507 build jobs successfully, then its warning gate rejected two deprecation warnings in SpecialPeriods11 and one long-line warning in Smale11. There were no Lean compiler errors in that shard.",
"prior_shard_url": "https://github.com/Vilin97/lean-pool/actions/runs/36230873820/job/108373745076",
"alias": "The pinned Mathlib declaration localInverse_contMDiffAt is exactly a deprecated alias of contMDiffAt_localInverse. Both call sites retain the same hq/e receiver and all composition/transport arguments.",
"primary_source": "https://github.com/leanprover-community/mathlib4/blob/c55e6e786f49471c72fbddbec5415808896aec1e/Mathlib/Geometry/Manifold/LocalDiffeomorph.lean",
"layout": "Smale.CoverNaturality.chainMap_comp retains identical non-whitespace tokens and the same map_comp proof."
},
"validation": {
"source": "Complete three containing proof contexts and the pinned alias inspected; independent parent source review passed. Exact replacement/whitespace checks cover every changed byte.",
"static": "All four existing scoped header, forbidden-text, file-size and proof-size gates pass on both files; every line in both files is at most 100 characters, and git diff --check passes. All 147 Hopf project paths remain, with the other 145 files byte-identical. Registry/card, root index/umbrella, imports, configurations and gates are unchanged; own card matches the registry.",
"limits": "No new local compiler, generator or full-project validation was run. The previous successful shard build describes the baseline only; fresh CI must validate this new head and the remaining shards."
},
"actions": "Normal guarded two-file push and this scoped comment only. Draft/body state preserved; no manifest, merge, CI queue, main-refresh, label or gate action."
}