Repositories, what they implement, and what they are not
This observatory does not host PDF manuscripts. Source and formalization live on GitHub. Some repositories are meant for other people to clone, build, and cite. Others are personal documentation of builds and process — kept so the author can track provenance — and are marked as such.
I. Open-source contribution
These public repositories are the pieces a third party can actually use: clone, build, fork, cite.
| Repo | What it implements | For the community |
|---|---|---|
| NS_Millennium_Proof Lean 4 · Apache-2.0 · CI |
Frohmanian Symplectic Tether as a two-layer Lean 4 project: geometric tether on coadjoint orbits (Modules/SymplecticTether.lean, Modules/ArnoldGeometric.lean) and an analytic tethered Lyapunov / independent-majorant layer (Modules/TetheredLyapunov.lean, Modules/IndependentMajorant.lean, Modules/GlobalRegularity.lean). Blueprint, LaTeX↔Lean map, CITATION.cff. |
A buildable formalization artifact with reusable lemmas under ForMathlib/ following the hygiene pattern of Tao’s PFR project — intended for eventual Mathlib upstreaming. Not a finished Clay proof; remaining analytic holes are marked sorry. |
| frohmanian-ns-symplectic-tether Apache-2.0 |
Public landing page for the tether program: core ideas, honest scope, pointer to the Lean corpus. | An index so searchers of “Frohmanian tether” land on the maintained Lean repo. It is not a library of code. |
II. Personal documentation and provenance
These exist so the author can keep tabs on dates, drafts, and process. They are not packages for other people to depend on.
| Repo / record | What it is | What it is not |
|---|---|---|
| frohmanian-tether-manuscript-2026-06-01 archived |
June 1, 2026 manuscript upload (main.tex + figures) — earliest public content record of the program. |
Not a living paper, not a package. Read-only provenance. |
| Test-Practice-Repo archived |
Practice upload of the Lean corpus on 19 June 2026, preserved read-only. | Not the active formalization. Use NS_Millennium_Proof. |
| Anagram reachability Zenodo · 2026-07 / 2026-08-19 |
Zero-sorry Lean 4 combinatorial engine (exact multiset cover, well-founded recursion) used as a laboratory for the same termination discipline as the tether work. |
Not a GitHub library and not a Mathlib submission. Personal working log, archived on Zenodo. |
| BenFrohman | Public GitHub profile README: identity, observatory link, sponsor line, corpus pointers. | Not research code. |
| .github | Default community-health files, GitHub Sponsors, and Ko-fi (FUNDING.yml) for the author’s public repositories. |
Not a product. |
III. Private — not open source
These are real builds the author tracks, but they are not contributions to the public commons. There is no public clone URL.
| Work | What it implements | Access |
|---|---|---|
| symplectohydronamics | Private source of this observatory (static HTML/CSS/WebGL). The compiled site is public; the working git is not. | This site. Source stays private. |
| overemployed-job-bot | Multi-tenant SaaS for remote AI job hunting: per-user sandboxes, scanners, 24h trial, Stripe $20 lifetime unlock. | Private GitHub repo. Product inquiry via consulting. |
| SealGuard | Containment and integrity architecture for agentic and infrastructure surfaces. | NDA only. Not on GitHub. |
How to cite
Cite the Lean corpus, not this HTML page: Frohmanian Symplectohydrodynamics (FSymHD) by Benjamin Stanley Frohman, ORCID 0009-0006-7068-3718, repository BenFrohman/NS_Millennium_Proof (CITATION.cff). Original FSymHD writing on this observatory is CC BY 4.0. The Lean corpus is Apache-2.0.
Support the independent program: GitHub Sponsors · Ko-fi (Frohmanian).
© 2026 Benjamin Stanley Frohman, original author. JAMA / JNS papers remain on the prior-research tab under those publishers’ copyrights and are not relicensed here.