A structural research program asking which maps connect arithmetic geometry, Weil positivity, polarisation, and spectral realization, and whether finite Connes/Weil approximations supply those maps.
Read the papers · Repository · Review record
This project does not prove the Riemann Hypothesis. It proves general transfer lemmas and counterexamples, audits existing formal interfaces, and specifies the arithmetic comparisons that remain unconstructed. The classical Weil functional and its equivalence with RH are defined and sourced in the papers; they are not yet formalized in this Lean library.
The central sufficient geometric package is a primitive space with a nonpositive intersection pairing I, an arithmetic test-function map Γ, and the exact signed comparison
Negativity then transfers directly to Weil positivity. The construction of that arithmetic space and comparison remains open. There is no claim of a category-independent minimal object over Spec Z. The universal Hilbert realization of a fixed Hermitian form exists exactly when the form is nonnegative, so its existence is a certificate equivalent to the sign condition.
Finite approximations have different conclusions. Smooth spectral sums converge without providing positivity. At fixed support the prime sum is finite and exact, while the full formula is signed. Positive finite models need maps from common tests and a vanishing comparison defect. Connes-style ground-state approximations require the precise real-zero hypotheses and a normalized holomorphic comparison with the actual ground state; convergence of the explicit proxy is a separate result.
| Paper | Pages | Focus | Read | Download |
|---|---|---|---|---|
| Arithmetic positivity structures | 20 | Primitive intersection and cohomological structures | Reader | |
| Finite Weil approximations | 23 | Convergence, operator comparisons, and remaining defects | Reader | |
| Structural arithmetic geometry | 20 | Universal realizations and maps between the criteria | Reader |
All 63 pages have canonical LaTeX sources and PDFs. The reader is generated from those sources.
Independent primitive sign + exact arithmetic map --> Weil positivity
Prescribed positive models + vanishing comparison --> Weil positivity
Weil positivity <--> universal positive realization
The first two arithmetic inputs remain unconstructed.
The third line is a certificate equivalence, not an independent proof.
The package contains 76 named theorems. The complete build passes; its kernel audit covers 132 theorem declarations, including generated declarations, and uses only propext, Classical.choice, and Quot.sound. It contains no new mathematical axioms, sorry, or opaque arithmetic predicates. Hypotheses appear in theorem parameters or explicit structures.
| Module | Scope |
|---|---|
| Structures | Exact comparison composition and positivity transfer; norm-square certificate equivalences; primitive intersection comparisons and a nonzero model. |
| Bridges | Primitive degree corrections; radical quotient and inner-product core; unique comparison factorization; countermodels for missing hypotheses. |
| Approximation | Approximate positivity, dense-core transfer, changing spaces, finite Gram limits, weighted transform estimates, shrinking-gap and subtraction counterexamples. |
| Spectral | An explicit adjoint weight identity forces the real part of represented eigenvalues, with domain and nonzero eigenvector hypotheses. |
| Residual | Eventual one-sided scalar comparison; unrestricted existential model certificates are equivalent to target nonnegativity. |
The forms in these declarations are explicit parameters. ArithmeticComparison exposes an equality; its name does not assert a number-theoretic identity. ApproximationCertificate does not assert that its model spaces are finite-dimensional. A concrete finite approximation must supply that additional structure. The radical quotient creates an inner-product core from supplied positivity; it does not prove arithmetic positivity or construct a complete arithmetic cohomology.
Requires Lean's elan toolchain manager. Lean is pinned to v4.30.0-rc2; mathlib is pinned to commit 0f9072dd907c6e2e4264ab241a049cab50137f7c and dependency revisions are committed.
cd lean
lake exe cache get
lake build
lake env lean ../scripts/audit-lean.leanThe axiom audit writes research/lean-axiom-audit.json and rejects dependencies beyond propext, Classical.choice, and Quot.sound. Its theorem count includes generated Lean declarations; the named theorem inventory is recorded separately. The local development checkout may reuse a pinned mathlib cache, but that cache is ignored by git and is not required by a fresh clone.
Compile each .tex file twice with pdflatex, writing to papers/pdf. The reader uses Next.js, TypeScript and KaTeX, hosted on Vercel. Matching committed content and image caches allow an ordinary build with Node.js and npm. Fresh LaTeX conversion and content regression tests also require Pandoc; regenerating preview cards requires ImageMagick. Conversion renders KaTeX strictly and verifies source-derived formula, row and label inventories.
cd website
npm ci
npm run build
npm run check
npm run verifyThe committed lockfile pins the web dependencies. The content label cache is tied to the LaTeX source hash; changing a manuscript requires recompilation before conversion. The build rejects unsupported mathematics. Run npm run test:content to exercise the ten content-integrity tests, including deliberate deletion of inline formulas, display formulas, alignment rows and unreferenced labels.
The Lean audit, named theorem inventory, paper integration check, and publication preflight record their exact scope. External Codex reviews passed for the Lean code and the corrected website. Two HTML/math fixers checked the reader; all eight desktop/mobile browser cases pass. Live HTTP and byte comparisons passed for sixteen routes and assets in the deployment check.
The original AGY reviews returned ACCEPT for Part I and MINOR REVISIONS for Parts II and III. Valid corrections were implemented, and reviewers who did not author the respective papers checked the final changes. An additional combined AGY recheck was rejected by its freshness guard and is not counted as an acceptance. The full distinction is in the review summary. These are AI-assisted reviews of a research program, not journal acceptance or proof of the open arithmetic construction.
The five input repositories are read-only context, pinned in research/source-revisions.json. Their proposition-level Gap A/Gap B equivalence passes through RH; the audit does not treat it as a direct comparison of pairings. The stopped riemann-hypothesis-proof project was preserved as a separate directory and is not resumed by APP.
Primary literature includes Connes–Consani–Moscovici, Zeta spectral triples, Connes–van Suijlekom, Quadratic forms and real zeros, and Suzuki, Weil's quadratic form via the screw function. Claim scopes and current limitations are recorded in research, with external reviews in reviews.
Matthew Long and the YonedaAI Collaboration. September 2026.