Opera Numerorum — Morning Star Project Manifest

DavidFox998 / Morning Star Project, Volume I

This repository is the canonical coordination index for all formal work across the Morning Star Project's Clay Millennium Prize towers.

---

Axiom Footprint (project-wide)

{propext, Classical.choice, Quot.sound}

No sorry, no admit, no native_decide in any registered brick. Every brick is machine-checkable with #print axioms <theorem>.

Lean Toolchain

leanprover/lean4:v4.12.0
mathlib: v4.12.0  (commit 809c3fb3b5c8f5d7dace56e200b426187516535a)

---

Tower Status

Problem	Repository	Active Bricks	Status
Yang–Mills Mass Gap	yang-mills-massgap	582	OPEN — YM Surface #1 unproved; scalar-shadow Hamiltonian only
RH Core C01–C07	rh-core-c01-c07	2	OPEN — conditional combinator; no zero-free region discharged
RH P5 Bridge / 14 Primes	rh-p5-bridge-14	2	OPEN — ZeroDensity brick + ZProtocol honesty bridge
Birch–Swinnerton-Dyer	Birch-and-Swinnerton-Dyer	0	OPEN — MordellWeil stub; no rank or L-function result
Navier–Stokes	navier-stokes	80	OPEN — energy scaffold; global regularity unproved; FROZEN
Hodge	hodge-abelian-boundaries	0	OPEN — abelian boundary scaffold
Lindelöf / RH support	lindelof-mu-bound	TBD	OPEN — supporting computation
Bost–Connes	bost-connes	1	WIP — bost_connes_threshold numerical fact only
P vs NP	p-vs-np	0	Reserved — exploratory scaffolding, no proof
Total		~664

What a "brick" means: a Lean theorem that compiles with axioms = classical trio and sorry = 0. A brick is necessary but not sufficient toward the Clay surface above it. Every Clay surface in this table is OPEN.

---

How to Verify

# Clone this environment
git clone https://github.com/DavidFox998/opera-numerorum

# Check all active bricks (exits 0 if all pass)
bash scripts/check-towers.sh

# Verify a specific theorem
cd lean-proof-towers
lake env lean Towers/YM/SU3Instances.lean
# then in Lean: #print axioms TheoremaAureum.Towers.YM.su3_lie_algebra_def

---

Documents

LaTeX source documents and PDF build CI: pistus-theoria

---

Honesty Statement

No Clay Millennium Prize problem has been solved by this project.

• YM Surface #1 (mass gap μ > 0): OPEN
• RH: OPEN
• BSD: OPEN
• NS Surface #1 (global regularity): OPEN
• Hodge: OPEN

The 664 verified Lean lemmas are real, honestly bounded results. They form necessary (not sufficient) conditions toward these surfaces.