Upgrade to mathlib 4.30 and fix Navier-Stokes target

[Robertboy18]

Fixes #5.

This updates the Navier-Stokes Millennium entry point so the four Fefferman alternatives are exposed as separate targets rather than bundled into a single Lean disjunction.

[Copilot]

Pull request overview

This PR upgrades the project to Lean 4.30 / mathlib 4.30 and adjusts the Navier–Stokes “Millennium problem” entry point so that Fefferman’s alternatives (A)–(D) are exposed as separate formal targets (addressing the formulation weakness described in issue #5).

Changes:

• Bump toolchain and dependency pins to Lean v4.30.0 and mathlib v4.30.0 (with updated lake manifest).
• Refactor Navier–Stokes Millennium target from a single disjunction into a structure of separate targets, and re-export A–D individually.
• Update imports / small compatibility edits across several problem files to match mathlib 4.30 module paths and definitions; remove the local TM2 polytime composition development and make P vs NP lemmas conditional on a composition-closure hypothesis.

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
README.md	Updates Navier–Stokes section to reflect separated A–D targets.
Problems/YangMills/Quantum.lean	Adjusts Schwartz space import path for mathlib 4.30.
Problems/PvsNP/TM2PolyTimeComp.lean	Removes the local axiom-free TM2 polytime composition development.
Problems/PvsNP/PolynomialHierarchy.lean	Updates computability import paths for mathlib 4.30.
Problems/PvsNP/Millennium.lean	Updates TM2 computability APIs/imports; makes Cook propositions conditional on a composition-closure hypothesis.
Problems/NavierStokes/MillenniumBoundedDomain.lean	Introduces FeffermanMillenniumProblems structure and publishes separated A–D targets.
Problems/NavierStokes/Millennium.lean	Re-exports the separated targets (A–D) instead of a single disjunction proposition.
Problems/NavierStokes/Imports.lean	Updates Schwartz space import path for mathlib 4.30.
Problems/NavierStokes/Definitions.lean	Minor simp-proof adjustments for updated mathlib lemmas.
Problems/NavierStokes/AdjointSpace.lean	Minor simp-proof adjustments for updated mathlib lemma landscape.
Problems/Hodge/Variety.lean	Marks definitions as noncomputable where needed for compatibility.
Problems/Hodge/Millennium.lean	Updates universe usage / type parameters to match revised scaffolding.
Problems/BirchSwinnertonDyer/Millennium.lean	Minor simp proof tweak.
lean-toolchain	Updates Lean toolchain to v4.30.0.
lakefile.toml	Pins mathlib to v4.30.0.
lake-manifest.json	Updates the locked dependency revisions for the upgraded toolchain/mathlib.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.