This repository was archived by the owner on Aug 9, 2026. It is now read-only.

Repository navigation

Test-Practice-Repo

Public archive

About

Practice upload of the NS_Millennium_Proof corpus (June 19, 2026) — preserved read-only for provenance. Active repo: BenFrohman/NS_Millennium_Proof

1 star

0 watching

Report repository

Name		Name	Last commit message	Last commit date
.vscode		.vscode
ForMathlib/NS		ForMathlib/NS
Modules		Modules
NS_Millennium_Proof		NS_Millennium_Proof
docs		docs
historical		historical
mermaid		mermaid
scripts		scripts
.gitignore		.gitignore
AUTHORS.md		AUTHORS.md
Blueprint.md		Blueprint.md
COPYRIGHT.md		COPYRIGHT.md
HISTORY.md		HISTORY.md
LICENSE		LICENSE
LaTeX_Lean_Relationship.md		LaTeX_Lean_Relationship.md
NS_Millennium_Proof.lean		NS_Millennium_Proof.lean
README.md		README.md
build.log		build.log
lake-manifest.json		lake-manifest.json
lakefile.lean		lakefile.lean
lean-toolchain		lean-toolchain

Repository files navigation

NS_Millennium_Proof — Frohmanian Symplectic Tether Regularity Theorem

Author: Benjamin Stanley Frohman (@Investor0x / Bit21)
Date: 2026

Formalization in Lean 4 of the global regularity for the 3D incompressible Navier–Stokes equations using the Frohmanian Symplectic Tether framework.

Status: Build clean. Geometric core complete. Remaining sorry placeholders in analytic estimates.

Structure

ForMathlib/NS/Tether.lean: Upstream-candidate geometric kernel.
Modules/: Core modules (SymplecticTether, GlobalRegularity, etc.).
Definitions/FrohmanianTether.lean: Canonical naming (𝔉𝕋).

See HISTORY.md, Blueprint.md, and LaTeX_Lean_Relationship.md for full details.

About

Practice upload of the NS_Millennium_Proof corpus (June 19, 2026) — preserved read-only for provenance. Active repo: BenFrohman/NS_Millennium_Proof

1 star

0 watching

Report repository

Releases

Sponsor this project

Packages

Used by

Contributors

Languages